Johannes ┼man Pohjola
Cited by
Cited by
Broadcast psi-calculi with an application to wireless protocols
J Borgstr÷m, S Huang, M Johansson, P Raabjerg, B Victor, ...
Software & Systems Modeling 14, 201-216, 2015
A verified generational garbage collector for CakeML
A Sandberg Ericsson, MO Myreen, J ┼man Pohjola
Journal of Automated Reasoning 63, 463-488, 2019
Kalas: A verified, end-to-end compiler for a choreographic language
J┼ Pohjola, A Gˇmez-Londo˝o, J Shaker, M Norrish
13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
Higher-order psi-calculi
J Parrow, J Borgstr÷m, P Raabjerg, J┼ Pohjola
Mathematical Structures in Computer Science 24 (2), e240203, 2014
Do you have space for dessert? A verified space cost semantics for CakeML programs
A Gˇmez-Londo˝o, J ┼man Pohjola, HT Syeda, MO Myreen, YK Tan
Proceedings of the ACM on Programming Languages 4 (OOPSLA), 1-29, 2020
Characteristic formulae for liveness properties of non-terminating CakeML programs
J ┼man Pohjola, H Rostedt, MO Myreen
10th International Conference on Interactive Theorem Proving (ITP 2019), 2019
Program verification in the presence of I/O: Semantics, verified library routines, and verified applications
H FÚrÚe, J ┼man Pohjola, R Kumar, S Owens, MO Myreen, S Ho
Verified Software. Theories, Tools, and Experiments: 10th Internationalá…, 2018
A mechanised semantics for HOL with ad-hoc overloading
J┼ Pohjola, A Gengelbach
arXiv preprint arXiv:2002.10212, 2020
A sorted semantic framework for applied process calculi
J Borgstr÷m, R Gutkovas, J Parrow, B Victor, J┼ Pohjola
Logical Methods in Computer Science 12, 2016
Negative premises in applied process calculi
J ┼man Pohjola, J Borgstr÷m, J Parrow, P Raabjerg, I Rodhe
Into the infinite-theory exploration for coinduction
SH Einarsdˇttir, M Johansson, J ┼man Pohjola
Artificial Intelligence and Symbolic Computation: 13th Internationalá…, 2018
PureCake: A verified compiler for a lazy functional language
H Kanabar, S Vivien, O Abrahamsson, MO Myreen, M Norrish, J┼ Pohjola, ...
Proceedings of the ACM on Programming Languages 7 (PLDI), 952-976, 2023
Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading
A Gengelbach, J┼ Pohjola, T Weber
arXiv preprint arXiv:2101.03807, 2021
Synthesis of verified architectural components for autonomy hosted on a verified microkernel
K Slind, DS Hardin, J┼ Pohjola, M Sproul
Draft, 2019
Bisimulation up-to techniques for psi-calculi
J ┼man Pohjola, J Parrow
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs andá…, 2016
Priorities without priorities: representing preemption in Psi-calculi
J┼ Pohjola, J Parrow
arXiv preprint arXiv:1408.1453, 2014
Towards Correctly Checking for Cycles in Overloaded Definitions
A Gengelbach, J┼ Pohjola
Department of Information Technology, Uppsala University, 2021
Verifying psi-calculi
J┼ Pohjola
Master’s thesis, Uppsala University, Department of Information Technology, 2010
Pancake: verified systems programming made sweeter
J┼ Pohjola, HT Syeda, M Tanaka, K Winter, TW Sau, B Nott, TT Ung, ...
Proceedings of the 12th Workshop on programming languages and operatingá…, 2023
Connecting choreography languages with verified stacks
A Gˇmez-Londono, J┼ Pohjola
Procs. of the Nordic Workshop on Programming Theory, 31-33, 2018
The system can't perform the operation now. Try again later.
Articles 1–20