Johannes Åman Pohjola
Lecturer
Research Interests
Johannes is interested in beauty and truth. He works on interactive theorem proving, program verification and concurrency theory, specifically for the Pancake language
Contact Details
| Email: | j.amanpohjola@unsw.edu.au |
|---|
More contact information is available at the Contact page.
Projects
Current |
Past |
Career Summary
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
Qualifications
MSc in Computer Science, Uppsala University, Sweden, 2010
PhD in Computer Science, Uppsala University, Sweden, 2016
Program Committees and Editorial Boards
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
Recognition and Awards
Best paper award at FORTE/DisCoTeC 2019
Publications
Trustworthy Systems Group Papers
2023
|
 |
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 |
2022
|
|
|
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 |
2020
|
|
|
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 |
2019
|
|
|
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 |
2018
|
|
|
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 |