Jonas Kastberg Hinrichsen

Jonas Kastberg Hinrichsen

Affiliation:   Logics and Semantics, Aarhus University, Denmark

Short Biography


I'm a reliable guy, currently acting at Aarhus University Denmark, serving a postdoc protocol. My interests revolve around certifying strong reliable guarantees about unreliable software via machine-checked mathematical verification; thus far primarily involving 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. I aim at bridging the gap between industry and academia, through research outputs that are widely accessible. My primary research contribution thus far---the Actris logical framework---is then, in part, a venture about certifying strong reliability for complicated message-passing systems, captured by specifications and proofs that are parsable by those who are less theoretically interested.


2024 POPL, Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement [pdf]

2024 POPL, Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing [pdf]

2023 ICFP, Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols [pdf]

2023 ICFP, Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl) [pdf]

2022 LMCS, Actris 2.0: Asynchronous Session-Type Based reasoning in Separation Logic [pdf]

2021 CPP, Machine-Checked Semantic Session Typing [Distinguished Paper Award] [pdf]

2020 POPL, Actris: Session-Type Based reasoning in Separation Logic [pdf]


Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic [pdf]

Multris: Functional Verification of Multiparty Message Passing in Separation Logic [pdf]

PhD Dissertation

Sessions and Separation [pdf]


2024, June 03, Iris Workshop [Invited talk] [Slides]

2024, May 14, Uppsala University [Slides]

2024, March 18, Aarhus University, Seminar [Slides]

2024, January 31, Dagstuhl Seminar [Coq Demo]

2023, September 07, ICFP Conference [Slides]

2023, May 23, Iris Workshop [Slides]

2023, March 03, Aarhus University, Iris Seminar [Slides]

2022, October 24, Aarhus University, Seminar [Slides]

2022, May 02, Iris Workshop [Slides]

2021, November 22, Aarhus University, Seminar [Slides]

2021, June 11, Ph.D. Defense [Slides]

2021, January 18, CPP Conference (short version) [Slides] [Recording] (long version) [Slides] [Recording]

2020, November 30, Aarhus University, Seminar [Slides]

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)

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


E-mail: hinrichsen at
Phone: +45 60 24 99 24
Office: Åbogade 34
8200 Aarhus N, DK-Denmark