Jonas Kastberg Hinrichsen
| Assistant Professor | Google Scholar | |
| Affiliation: | Computer Science Copenhagen, Aalborg University, Denmark |
Short Biography
My interests revolve around certifying strong reliable guarantees about unreliable software via machine-checked mathematical verification; thus far focusing on message-passing communication and distributed systems. I come from an applied background, having a software development degree, which skews my interests in the direction of the more pragmatically applicable. My vision is to bridge the gap between industry and academia, through research outputs that are widely accessible, achieved through modularity and abstraction. My primary research contribution thus far---the Actris logical framework---is a venture about certifying strong reliability for complicated message-passing systems via high-level specification and proof patterns.
Publications
| [10] | OOPSLA'26 |
Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing [Preprint]
Jonas Kastberg Hinrichsen, Iwan Quémerais, Lars Birkedal |
| [9] | CPP'26 |
Building Blocks for Step-Indexed Program Logics
Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers |
| [8] | OOPSLA'24 |
Multris: Functional Verification of Multiparty Message Passing in Separation Logic
Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers |
| [7] | POPL'24 |
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon Oddershede Gregersen, Leo Stefanesco, Jonas Kastberg Hinrichsen, Leon Gondelman, Abel Nieto, Lars Birkedal |
| [6] | POPL'24 |
Deadlock-Free Separation Logic: Linearity Yields Progress for
Dependent Higher-Order Message Passing
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers |
| [5] | ICFP'23 |
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
Leon Gondelman, Jonas Kastberg Hinrichsen, Mario Pereira, Amin Timany, Lars Birkedal |
| [4] | ICFP'23 |
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers |
| [3] | LMCS'22 |
Actris 2.0: Asynchronous Session-Type Based reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers |
| [2] | CPP'21 |
Machine-Checked Semantic Session Typing [Distinguished Paper Award]
Jonas Kastberg Hinrichsen, Daniel Louwrink, Robbert Krebbers, Jesper Bengtson |
| [1] | POPL'20 |
Actris: Session-Type Based reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers |
PhD Dissertation
Selected Talks
2025, December 11, IT University of Copenhagen, CISAT [Slides]
2025, February 25, Aalborg University, Seminar [Slides]
2024, June 03, Iris Workshop [Invited talk] [Slides]
2024, May 14, Uppsala University, Seminar [Slides]
2024, January 31, Dagstuhl Seminar [Coq Demo]
2023, September 07, ICFP Conference [Slides]
2023, May 23, Iris Workshop [Slides]
2022, October 24, Aarhus University, Seminar [Slides]
2022, May 02, Iris Workshop [Slides]
2021, June 11, Ph.D. Defense [Slides]
2021, January 18, CPP Conference (short version) [Slides] [Recording] (long version) [Slides] [Recording]
2020, November 18, Radboud University, Seminar [Slides]
2020, October 20, IT University of Copenhagen, Seminar [Slides]
2020, June 04, VEST workshop [Slides]
2020, May 27, Delft University of Technology, Seminar [Slides]
2020, January 22, POPL Conference [Slides] [Recording]
2019, October 28, Iris Workshop [Slides]
2019, October 02, Harvard University, Seminar [Slides]
Selected Teaching
2024, January 15, POPL Conference, Iris/Actris Tutorial [Slides]
2022, September 21, KU Leuven, Summer School on Security and Verification [Slides]
Conference Board and Commitee Participation
Research Article Evaluation (* External)
FORTE'26 · POPL'26 · ICE'25 · GandALF'24 · LICS'24* · FoSSaCS'24* · CPP'24* · POPL'24* · OOPSLA'22* · PLACES'22 · POPL'22*
Artifact Evaluation
ESOP'23 · PLDI'22 · POPL'22 · ICFP'20
Teaching Activities
Tutorial Responsible, Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types, POPL′24 TutorialFest
Presenter - Summer School on Security Testing and Verification, KU Leuven, September 2022
Course Instructor - Program Logics, Aarhus University, Fall 2022
Course Instructor - Program Logics, Aarhus University, Fall 2021
Course Instructor - Advanced Programming, IT University of Copenhagen, Fall 2018
Course Instructor - Programming Language Concepts and Implementation, IT University of Copenhagen, Spring 2018
Teaching Assistant - Intelligent Systems Programming, IT University of Copenhagen, Spring 2016
Teaching Assistant - Operative Systems and C, IT University of Copenhagen, Fall 2015
Industry Activities
Formal Methods Developer at Bedrock Systems, Inc., Fall 2019
Contact
| E-mail: | jkhi at cs.aau.dk | |
| Office: | A. C. Meyers Vænge 15 | |
| 2450 København, DK-Denmark | ||