Trustworthy Systems

Johannes Åman Pohjola

Research Interests

Johannes is interested in beauty and truth. Specifically, he works on interactive theorem proving, program verification and concurrency theory.

Contact Details

More contact information is available at the Contact page.

Photo of Johannes Åman Pohjola

Publication List



Career Summary

2010-2016: PhD student at Uppsala University, Sweden

2016-2018: Postdoctoral researcher at Chalmers University of Technology, Sweden


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


Trustworthy Systems Group Papers


Abstract PDF 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
Abstract PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF 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


Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Johannes Åman Pohjola
Psi-calculi revisited: Connectivity and compositionality
Technical Report, Data61, CSIRO, April, 2019


Abstract PDF 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: Theory, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018
Abstract PDF Alejandro Gomez-Londono and Johannes Åman Pohjola
Connecting choreography languages with verified stacks
at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018
Abstract PDF 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