A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract). - Johannes Borgström; Ramunas Gutkovas; Joachim Parrow; Björn Victor; Johannes Åman Pohjola (TGC, 2013)

Priorities Without Priorities: Representing Preemption in Psi-Calculi. - Johannes Åman Pohjola; Joachim Parrow (EXPRESS/SOS, 2014)

Higher-order psi-calculi. - Joachim Parrow; Johannes Borgström; Palle Raabjerg; Johannes Åman Pohjola (Math. Struct. Comput. Sci., 2014)

Broadcast psi-calculi with an application to wireless protocols. - Johannes Borgström; Shuqin Huang; Magnus Johansson; Palle Raabjerg; Björn Victor; Johannes Åman Pohjola; Joachim Parrow (Softw. Syst. Model., 2015)

Bisimulation up-to techniques for psi-calculi. - Johannes Åman Pohjola; Joachim Parrow (CPP, 2016)

The Expressive Power of Monotonic Parallel Composition. - Johannes Åman Pohjola; Joachim Parrow (ESOP, 2016)

A Sorted Semantic Framework for Applied Process Calculi. - Johannes Borgström; Ramunas Gutkovas; Joachim Parrow; Björn Victor; Johannes Åman Pohjola (Log. Methods Comput. Sci., 2016)

Culling Concurrency Theory : Reusable and trustworthy meta-theory, proof techniques and separation results. - Johannes Åman Pohjola (2016)

Into the Infinite - Theory Exploration for Coinduction. - Sólrún Halla Einarsdóttir; Moa Johansson; Johannes Åman Pohjola (AISC, 2018)

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. - Hugo Férée; Johannes Åman Pohjola; Ramana Kumar; Scott Owens; Magnus O. Myreen; Son Ho (VSTTE, 2018)

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. - Johannes Åman Pohjola; Henrik Rostedt; Magnus O. Myreen (ITP, 2019)

A Verified Generational Garbage Collector for CakeML. - Adam Sandberg Ericsson; Magnus O. Myreen; Johannes Åman Pohjola (J. Autom. Reason., 2019)

A Mechanised Semantics for HOL with Ad-hoc Overloading. - Johannes Åman Pohjola; Arve Gengelbach (LPAR, 2020)

Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. - Arve Gengelbach; Johannes Åman Pohjola; Tjark Weber (LFMTP, 2020)

Psi-Calculi Revisited: Connectivity and Compositionality. - Johannes Åman Pohjola (Log. Methods Comput. Sci., 2020)

Do you have space for dessert? a verified space cost semantics for CakeML programs. - Alejandro Gómez-Londoño; Johannes Åman Pohjola; Hira Taqdees Syeda; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2020)

A Verified Cyclicity Checker: For Theories with Overloaded Constants. - Arve Gengelbach; Johannes Åman Pohjola (ITP, 2022)

Kalas: A Verified, End-To-End Compiler for a Choreographic Language. - Johannes Åman Pohjola; Alejandro Gómez-Londoño; James Shaker; Michael Norrish (ITP, 2022)

Pancake: Verified Systems Programming Made Sweeter. - Johannes Åman Pohjola; Hira Taqdees Syeda; Miki Tanaka; Krishnan Winter; Tsun Wang Sau; Benjamin Nott; Tiana J. Tsang Ung; Craig McLaughlin; Remy Seassau; Magnus O. Myreen; Michael Norrish; Gernot Heiser (PLOS@SOSP, 2023)

A Hoare Logic for Diverging Programs. - Johannes Åman Pohjola; Magnus O. Myreen; Miki Tanaka (Arch. Formal Proofs, 2023)

PureCake: A Verified Compiler for a Lazy Functional Language. - Hrutvik Kanabar; Samuel Vivien; Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Johannes Åman Pohjola; Riccardo Zanetti (Proc. ACM Program. Lang., 2023)

Broadcast Psi-calculi. - Palle Raabjerg; Johannes Åman Pohjola; Tjark Weber (Arch. Formal Proofs, 2024)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)

Fast, Verified Computation for HOL ITPs. - Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Hrutvik Kanabar; Johannes Åman Pohjola (J. Autom. Reason., 2025)