Johannes Åman Pohjola

31 papers A 1B 8C 2Misc 1Journal 13Unranked 5
YearRankTypeTitle / Venue / Authors
2025 C conf
A Rely-Guarantee-Based Simulation for Cooperative Semantics.
ICTAC
Kevin Tran, Johannes Åman Pohjola, Robert Sison, Gerwin Klein
2025 B conf
A Verified Cost Model for Call-By-Push-Value.
ITP
Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah
2025 J jnl
Fast, Verified Computation for HOL ITPs.
J. Autom. Reason.
Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola
2025 J jnl
Verifying Device Drivers with Pancake.
CoRR
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, Gernot Heiser
2024 J jnl
Broadcast Psi-calculi.
Arch. Formal Proofs
Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber
2023 J jnl
A Hoare Logic for Diverging Programs.
Arch. Formal Proofs
Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka
2023 — conf
Pancake: Verified Systems Programming Made Sweeter.
PLOS@SOSP
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
2023 J jnl
PureCake: A Verified Compiler for a Lazy Functional Language.
Proc. ACM Program. Lang.
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti
2022 B conf
A Verified Cyclicity Checker: For Theories with Overloaded Constants.
ITP
Arve Gengelbach, Johannes Åman Pohjola
2022 B conf
Kalas: A Verified, End-To-End Compiler for a Choreographic Language.
ITP
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish
2020 B conf
A Mechanised Semantics for HOL with Ad-hoc Overloading.
LPAR
Johannes Åman Pohjola, Arve Gengelbach
2020 J jnl
A Mechanised Semantics for HOL with Ad-hoc Overloading.
CoRR
Johannes Åman Pohjola, Arve Gengelbach
2020 J jnl
Do you have space for dessert? a verified space cost semantics for CakeML programs.
Proc. ACM Program. Lang.
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan
2020 — conf
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.
LFMTP
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
2020 J jnl
Psi-Calculi Revisited: Connectivity and Compositionality.
Log. Methods Comput. Sci.
Johannes Åman Pohjola
2019 J jnl
A Verified Generational Garbage Collector for CakeML.
J. Autom. Reason.
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
2019 B conf
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs.
ITP
Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen
2019 C conf
Psi-Calculi Revisited: Connectivity and Compositionality.
FORTE
Johannes Åman Pohjola
2019 J jnl
Psi-Calculi Revisited: Connectivity and Compositionality.
CoRR
Johannes Åman Pohjola
2018 Misc conf
Into the Infinite - Theory Exploration for Coinduction.
AISC
Sólrún Halla Einarsdóttir, Moa Johansson, Johannes Åman Pohjola
2018 — conf
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
VSTTE
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
2017 B conf
A Verified Generational Garbage Collector for CakeML.
ITP
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
2016 J jnl
A Sorted Semantic Framework for Applied Process Calculi.
Log. Methods Comput. Sci.
Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, Johannes Åman Pohjola
2016 B conf
Bisimulation up-to techniques for psi-calculi.
CPP
Johannes Åman Pohjola, Joachim Parrow
2016 — —
Culling Concurrency Theory : Reusable and trustworthy meta-theory, proof techniques and separation results.
Johannes Åman Pohjola
2016 A conf
The Expressive Power of Monotonic Parallel Composition.
ESOP
Johannes Åman Pohjola, Joachim Parrow
2015 J jnl
Broadcast psi-calculi with an application to wireless protocols.
Softw. Syst. Model.
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, Joachim Parrow
2014 J jnl
Higher-order psi-calculi.
Math. Struct. Comput. Sci.
Joachim Parrow, Johannes Borgström, Palle Raabjerg, Johannes Åman Pohjola
2014 — conf
Priorities Without Priorities: Representing Preemption in Psi-Calculi.
EXPRESS/SOS
Johannes Åman Pohjola, Joachim Parrow
2013 — conf
A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract).
TGC
Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, Johannes Åman Pohjola
2011 B conf
Broadcast Psi-calculi with an Application to Wireless Protocols.
SEFM
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, Joachim Parrow