publications

Complete list of my peer-reviewed publications, as well as selected other works

Publications under Review

Pre-prints of papers currently under submission.

  1. Tree Borrows
    Neven Villani, Johannes Hostert, Derek Dreyer, and Ralf Jung
    In TBA, Slides from Talk at Rust Verification Workshop, 2024
    PDF Slides Code

Peer-Reviewed Publications

  1. A Program Logic for Verified Interoperability Between OCaml and C
    Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer
    Proceedings of the ACM on Programming Languages, 7, OOPSLA2, 2023
    DOI PDF Slides Video Code Website
  2. Undecidability of Dyadic First-Order Logic in Coq
    Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst
    13th International Conference on Interactive Theorem Proving (ITP), 2022
    DOI PDF Slides Code Website

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.

  1. 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
    PDF Slides Code
  2. A Toolbox for Mechanised First-Order Logic
    Johannes Hostert, Mark Koch, and Dominik Kirst
    In The Coq Workshop, 2021
    PDF Slides Video

Theses

  1. Logical Foundations Of Language Interoperability Between OCaml And C
    Johannes Hostert
    Master’s Thesis, Saarland University, 2023
    DOI PDF Slides Code Supp Website Awarded
  2. The Undecidability of First-Order Logic over Small Signatures
    Johannes Hostert
    Bachelor’s Thesis, Saarland University, 2021
    PDF Slides Website Awarded

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.