Peer-Reviewed Publications
-
Completeness of Iris-Based Program Logics
Proceedings of the ACM on Programming Languages, 10, ICFP, 2026
-
Tree Borrows
Proceedings of the ACM on Programming Languages, 9, PLDI, 2025
-
A Program Logic for Verified Interoperability Between OCaml and C
Proceedings of the ACM on Programming Languages, 7, OOPSLA2, 2023
-
Undecidability of Dyadic First-Order Logic in Coq
13th International Conference on Interactive Theorem Proving (ITP), 2022
Workshop Presentations and Other Talks
Selected talks only. Not all talks were held by me, but all are about work I was significantly involved in.
-
A Coq Library for Mechanised First-Order Logic
Dominik Kirst,
Johannes Hostert,
Andrej Dudenhefner,
Yannick Forster,
Marc Hermes,
Mark Koch,
Dominique Larchey-Wendling,
Niklas Mück,
Benjamin Peters,
Gert Smolka, and others
In The Coq Workshop, 2022
-
Theses
-
Logical Foundations Of Language Interoperability Between OCaml And C
Johannes Hostert
Master’s Thesis, Saarland University, 2023
-
The Undecidability of First-Order Logic over Small Signatures
Johannes Hostert
Bachelor’s Thesis, Saarland University, 2021
Other Material
At Saarland University, I contributed to re-writing the lecture notes used in the Maths Prep Course, a preparatory course for incoming freshmen completely organized by volunteer students from higher years. Nearly 200 students take this course every year, and they catch up on formal logic, proofs, sets, and induction, while also getting accustomed to the university early. The course has its own lecture notes, where chapter 2 and 3 were mainly written by me.