Jonas Kastberg Hinrichsen
| Postdoc | ||
| Affiliation: | Programming, Logic, and Semantics, IT University of Copenhagen, 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
2024 OOPSLA, Multris: Functional Verification of Multiparty Message Passing in Separation Logic [pdf]
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]
Manuscripts
Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic [pdf]
PhD Dissertation
Sessions and Separation [pdf]
Talks
2024, December 3, IT University of Copenhagen, Seminar [Slides]
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)
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: | jkas at itu.dk | |
| Office: | Rued Langgaards Vej 7 | |
| 2300 København S, DK-Denmark | ||