Johannes is interested in beauty and truth. He works on interactive theorem proving, program verification and concurrency theory, specifically for the Pancake language
| Email: | j.amanpohjola@unsw.edu.au |
|---|
More contact information is available at the Contact page.
Current |
Past |
2010-2016: PhD student at Uppsala University, Sweden
2016-2018: Postdoctoral researcher at Chalmers University of Technology, Sweden
2018-2021: Research Scientist, CSIRO's Data61, Sydney
MSc in Computer Science, Uppsala University, Sweden, 2010
PhD in Computer Science, Uppsala University, Sweden, 2016
ICE 2017 : 10th Interaction and Concurrency Experience
EXPRESS/SOS 2017 : Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics
ICE 2019 : 12th Interaction and Concurrency Experience
Best paper award at FORTE/DisCoTeC 2019
|
|
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023 |
|
|
|
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti Purecake: A verified compiler for a lazy functional language Proc. ACM Program. Lang., Volume 7, Number PLDI, pp. 952–976, 2023 |
|
|
|
Arve Gengelbach and Johannes Åman Pohjola A verified cyclicity checker: For theories with overloaded constants Proceedings of the 13th International Conference on Interactive Theorem Proving, pp. 15:1–15:18, Haifa, Israel, August, 2022 |
|
|
|
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish Kalas: A verified, end-to-end compiler for a choreographic language Proceedings of the 13th International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 2022 |
|
 |
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Logical Methods in Computer Science, Volume 16, Issue 4, pp. 16:1-16:28, December, 2020 |
|
|
 |
Alejandro Gomez-Londono, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus Myreen and Yong Kiam Tan Do you have space for dessert? A verified space cost semantics for CakeML programs OOPSLA, pp. 204:1-29, Chicago, IL, November, 2020 |
|
|
|
Johannes Åman Pohjola and Arve Gengelbach A mechanised semantics for HOL with ad-hoc overloading LPAR23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 498-515, Alicante, Spain, May, 2020 |
|
|
|
Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul Synthesis of verified architectural components for autonomy hosted on a verified microkernel Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020 |
|
|
|
Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen Characteristic formulae for liveness properties of non-terminating CakeML programs Proceedings of the 10th International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019 |
|
|
|
Adam Sandberg Ericsson, Magnus Myreen and Johannes Åman Pohjola A verified generational garbage collector for CakeML Journal of Automated Reasoning, Volume 63, Issue 2, pp. 463–488, August, 2019 |
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality FORTE 2019: International Conference on Formal Techniques for Distributed Systems, pp. 3-20, Lyngby, Denmark, June, 2019 Best paper award |
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Technical Report, Data61, CSIRO, April, 2019 |
|
|
|
Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho Program verification in the presence of I/O: semantics, verified library routines, and verified applications Verified Software: Theories, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018 |
|
|
|
Alejandro Gomez-Londono and Johannes Åman Pohjola Connecting choreography languages with verified stacks at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018 |
|
|
|
Solrun Halla Einarsdottir, Moa Johansson and Johannes Åman Pohjola Into the infinite - theory exploration for coinduction Artificial Intelligence and Symbolic Computation, pp. 70-86, Suzhou, China, 2018 |