麻豆社madou

Dr Johannes Aman Pohjola

Dr Johannes Aman Pohjola

Conjoint Lecturer

MSc in Computer Science, Uppsala University, Sweden, 2010

PhD in Computer Science, Uppsala University, Sweden, 2016

Engineering
Computer Science and Engineering

Johannes 脜man Pohjola is interested in beauty and truth. Specifically, he is an education focussed lecturer, with research interests in interactive theorem proving, program verification and concurrency theory.

  • Book Chapters | 2019
    Pohjola J脜, 2019, 'Psi-Calculi Revisited: Connectivity and Compositionality.', in P茅rez JA; Yoshida N (ed.), Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings, Springer, pp. 3 - 20,
    Book Chapters | 2014
    Borgstr枚m J; Gutkovas R; Parrow J; Victor B; Pohjola JA, 2014, 'A sorted semantic framework for applied process calculi (extended abstract)', in , pp. 103 - 118,
    Book Chapters | 2014
    Borgstr枚m J; Gutkovas R; Parrow J; Victor B; Pohjola J脜, 2014, 'A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract)', in Trustworthy Global Computing, Springer International Publishing, pp. 103 - 118,
  • Journal articles | 2023
    Kanabar H; Vivien S; Abrahamsson O; Myreen MO; Norrish M; JOHANNES 脜MAN PA; Zanetti R, 2023, 'PureCake: A Verified Compiler for a Lazy Functional Language', Proceedings of the ACM on Programming Languages, 7,
    Journal articles | 2023
    Pohjola J脜; Myreen MO; Tanaka M, 2023, 'A Hoare Logic for Diverging Programs.', Arch. Formal Proofs, 2023
    Journal articles | 2021
    Gengelbach A; Pohjola J脜; Weber T, 2021, 'Mechanisation of model-theoretic conservative extension for HOL with Ad-hoc overloading', Electronic Proceedings in Theoretical Computer Science, EPTCS, 332, pp. 1 - 17,
    Journal articles | 2020
    G贸mez-Londo帽o A; 脜man Pohjola J; Syeda HT; Myreen MO; Tan YK, 2020, 'Do you have space for dessert? a verified space cost semantics for CakeML programs', Proceedings of the ACM on Programming Languages, 4,
    Journal articles | 2020
    Pohjola J脜; Gengelbach A, 2020, 'A mechanised semantics for hol with ad-hoc overloading', EPiC Series in Computing, 73, pp. 498 - 515,
    Journal articles | 2020
    Pohjola J脜, 2020, 'Psi-calculi revisited: Connectivity and compositionality', Logical Methods in Computer Science, 16, pp. 16:1-16:28,
    Journal articles | 2019
    Sandberg Ericsson A; Myreen MO; 脜man Pohjola J, 2019, 'A Verified Generational Garbage Collector for CakeML', Journal of Automated Reasoning, 63, pp. 463 - 488,
    Journal articles | 2016
    Borgstr枚m J; Gutkovas R; Parrow J; Victor B; Pohjola J脜, 2016, 'A sorted semantic framework for applied process calculi', Logical Methods in Computer Science, 12,
    Journal articles | 2015
    Borgstr枚m J; Huang S; Johansson M; Raabjerg P; Victor B; 脜man聽Pohjola J; Parrow J, 2015, 'Broadcast psi-calculi with an application to wireless protocols', Software and Systems Modeling, 14, pp. 201 - 216,
    Journal articles | 2014
    Parrow J; Borgstr枚m J; Raabjerg P; 脜man Pohjola J, 2014, 'Higher-order psi-calculi', Mathematical Structures in Computer Science, 24,
    Journal articles | 2014
    Pohjola J脜; Parrow J, 2014, 'PrioritiesWithout priorities: Representing preemption in psi-calculi', Electronic Proceedings in Theoretical Computer Science, EPTCS, 160, pp. 2 - 15,
  • Conference Papers | 2023
    Pohjola J脜; Syeda HT; Tanaka M; Winter K; Sau TW; Nott B; Ung TJT; McLaughlin C; Seassau R; Myreen MO; Norrish M; Heiser G, 2023, 'Pancake: Verified Systems Programming Made Sweeter.', in PLOS@SOSP, ACM, pp. 1 - 9,
    Conference Papers | 2023
    Pohjola J脜; Syeda HT; Tanaka M; Winter K; Sau TW; Nott B; Ung TT; McLaughlin C; Seassau R; Myreen MO; Norrish M; Heiser G, 2023, 'Pancake: Verified Systems Programming Made Sweeter', in PLOS 2023 - Proceedings of the 12th Workshop on Programming Languages and Operating Systems, Part of: SOSP 2023, pp. 1 - 9,
    Conference Papers | 2022
    Gengelbach A; Pohjola J脜, 2022, 'A Verified Cyclicity Checker For Theories with Overloaded Constants', in Leibniz International Proceedings in Informatics, LIPIcs,
    Conference Papers | 2022
    Pohjola J脜; G贸mez-Londo帽o A; Shaker J; Norrish M, 2022, 'Kalas: A Verified, End-To-End Compiler for a Choreographic Language', in Leibniz International Proceedings in Informatics, LIPIcs,
    Conference Papers | 2020
    Hardin D; Slind K; Pohjola J脜; Sproul M, 2020, 'Synthesis of verified architectural components for critical systems hosted on a verified microkernel', in Proceedings of the Annual Hawaii International Conference on System Sciences, pp. 6365 - 6374
    Conference Papers | 2019
    Pohjola J脜; Rostedt H; Myreen MO, 2019, 'Characteristic formulae for liveness properties of non-terminating CakeML programs', in Leibniz International Proceedings in Informatics, LIPIcs,
    Conference Papers | 2019
    脜man Pohjola J, 2019, 'Psi-Calculi Revisited: Connectivity and Compositionality', in Formal techniques for distributed objects, components, and systems : 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019 (Series title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Kongens Lyngby, Denmark, pp. 3 - 20, presented at FORTE, Kongens Lyngby, Denmark, 17 June 2019 - 21 June 2019,
    Conference Papers | 2018
    Einarsd贸ttir SH; Johansson M; 脜man Pohjola J, 2018, 'Into the infinite - theory exploration for coinduction', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 70 - 86,
    Conference Papers | 2018
    F茅r茅e H; 脜man Pohjola J; Kumar R; Owens S; Myreen MO; Ho S, 2018, 'Program Verification in the Presence of I/O: Semantics, Verified Library Routines, and Verified Applications', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, Oxford, U.K., pp. 88 - 111, presented at 10th International Conference, VSTTE 2018, Oxford, U.K., 18 July 2018 - 19 July 2018,
    Conference Papers | 2017
    Sandberg Ericsson A; Myreen MO; 脜man Pohjola J, 2017, 'A verified generational garbage collector for CakeML', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 444 - 461,
    Conference Papers | 2016
    Pohjola J脜; Parrow J, 2016, 'Bisimulation up-to techniques for psi-calculi', in CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016, pp. 142 - 153,
    Conference Papers | 2016
    Pohjola J脜; Parrow J, 2016, 'The expressive power of monotonic parallel composition', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 780 - 803,
    Conference Papers | 2011
    Borgstr枚m J; Huang S; Johansson M; Raabjerg P; Victor B; 脜man Pohjola J; Parrow J, 2011, 'Broadcast psi-calculi with an application to wireless protocols', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 74 - 89,

Best paper award at FORTE/DisCoTeC 2019