Jonas Kastberg Hinrichsen
| Postdoc | ||
| Affiliation: | Logics and Semantics, Aarhus University, Denmark |
Short Biography
I'm a reliable guy, most recently 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.
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, 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
Contact
| E-mail: | hinrichsen at cs.au.dk | |
| Phone: | +45 60 24 99 24 | |
| Office: | Åbogade 34 | |
| 8200 Aarhus N, DK-Denmark | ||