| 2021 | ITP | A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. | Andreas Lochbihler |
| 2020 | CADE | Quotients of Bounded Natural Functors. | Basil Frer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel |
| 2020 | CAV | Authenticated Data Structures as Functors in Isabelle/HOL. | Andreas Lochbihler, Ognjen Maric |
| 2018 | ITP | Fast Machine Words in Isabelle/HOL. | Andreas Lochbihler |
| 2018 | ITP | Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. | Andreas Lochbihler, Joshua Schneider |
| 2017 | ESOP | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. | Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | ITP | Effect Polymorphism in Higher-Order Logic (Proof Pearl). | Andreas Lochbihler |
| 2016 | ESOP | Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. | Andreas Lochbihler |
| 2016 | ITP | Equational Reasoning with Applicative Functors. | Andreas Lochbihler, Joshua Schneider |
| 2015 | ITP | A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. | Johannes Hlzl, Andreas Lochbihler, Dmitriy Traytel |
| 2015 | ITP | Stream Fusion for Isabelle's Code Generator - Rough Diamond. | Andreas Lochbihler, Alexandra Maximova |
| 2014 | ITP | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Recursive Functions on Lazy Lists via Domains and Topologies. | Andreas Lochbihler, Johannes Hlzl |
| 2013 | ITP | Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. | Andreas Lochbihler |
| 2012 | ESOP | Java and the Java Memory Model - A Unified, Machine-Checked Formalisation. | Andreas Lochbihler |
| 2011 | ITP | Animating the Formalised Semantics of a Java-Like Language. | Andreas Lochbihler, Lukas Bulwahn |
| 2010 | ESOP | Verifying a Compiler for Java Threads. | Andreas Lochbihler |
| 2010 | ITP | The Isabelle Collections Framework. | Peter Lammich, Andreas Lochbihler |
| 2007 | SCAM | On Temporal Path Conditions in Dependence Graphs. | Andreas Lochbihler, Gregor Snelting |