This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Johannes Hostert
A grouping.
Mechanised proofs: undecidability results and a Coq library with Kirst and others, and the first completeness result for Iris-based separation logics. The 2026 record is mechanised in Rocq while the 2022 pair are in Coq -- the same system, renamed -- so a search on either word returns some of this work and not the rest.
3 references
Completeness of Iris-Based Program Logics
Johannes Hostert and others (2026) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery (ACM)
Undecidability of dyadic first-order logic in Coq
Johannes Hostert and others (2022) · 13th International Conference on Interactive Theorem Proving (ITP 2022) · Schloss Dagstuhl – Leibniz-Zentrum für Informatik
A Coq Library for Mechanised First-Order Logic
Dominik Kirst and others (2022) · The Coq Workshop 2022