Jinja with Threads. - Andreas Lochbihler (Arch. Formal Proofs, 2007)

Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. - Daniel Wasserrab; Andreas Lochbihler (TPHOLs, 2008)

The computational complexity of evolutionarily stable strategies. - Kousha Etessami; Andreas Lochbihler (Int. J. Game Theory, 2008)

Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. - Andreas Lochbihler (TPHOLs, 2009)

Code Generation for Functions as Data. - Andreas Lochbihler (Arch. Formal Proofs, 2009)

On temporal path conditions in dependence graphs. - Andreas Lochbihler; Gregor Snelting (Autom. Softw. Eng., 2009)

Verifying a Compiler for Java Threads. - Andreas Lochbihler (ESOP, 2010)

The Isabelle Collections Framework. - Peter Lammich; Andreas Lochbihler (ITP, 2010)

Gateway Decompositions for Constrained Reachability Problems. - Bastian Katz; Marcus Krug; Andreas Lochbihler; Ignaz Rutter; Gregor Snelting; Dorothea Wagner (SEA, 2010)

Coinductive. - Andreas Lochbihler (Arch. Formal Proofs, 2010)

Animating the Formalised Semantics of a Java-Like Language. - Andreas Lochbihler; Lukas Bulwahn (ITP, 2011)

Java and the Java Memory Model - A Unified, Machine-Checked Formalisation. - Andreas Lochbihler (ESOP, 2012)

Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. - Andreas Lochbihler (Ausgezeichnete Informatikdissertationen, 2012)

A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. - Andreas Lochbihler (KIT Scientific Publ., 2012)

Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. - Andreas Lochbihler (ITP, 2013)

Light-weight Containers. - Andreas Lochbihler (Arch. Formal Proofs, 2013)

Native Word. - Andreas Lochbihler (Arch. Formal Proofs, 2013)

Making the java memory model safe. - Andreas Lochbihler (ACM Trans. Program. Lang. Syst., 2013)

Truly Modular (Co)datatypes for Isabelle/HOL. - Jasmin Christian Blanchette; Johannes Hölzl; Andreas Lochbihler; Lorenz Panny; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Recursive Functions on Lazy Lists via Domains and Topologies. - Andreas Lochbihler; Johannes Hölzl (ITP, 2014)

Stream Fusion in HOL with Code Generation. - Andreas Lochbihler; Alexandra Maximova (Arch. Formal Proofs, 2014)

Analysing Java's safety guarantees under concurrency. - Andreas Lochbihler (it Inf. Technol., 2014)

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. - Johannes Hölzl; Andreas Lochbihler; Dmitriy Traytel (ITP, 2015)

Stream Fusion for Isabelle's Code Generator - Rough Diamond. - Andreas Lochbihler; Alexandra Maximova (ITP, 2015)

The Stern-Brocot Tree. - Peter Gammie; Andreas Lochbihler (Arch. Formal Proofs, 2015)

A Zoo of Probabilistic Systems. - Johannes Hölzl; Andreas Lochbihler; Dmitriy Traytel (Arch. Formal Proofs, 2015)

Trie. - Andreas Lochbihler; Tobias Nipkow (Arch. Formal Proofs, 2015)

Applicative Lifting. - Andreas Lochbihler; Joshua Schneider 001 (Arch. Formal Proofs, 2015)

Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. - Andreas Lochbihler (ESOP, 2016)

Equational Reasoning with Applicative Functors. - Andreas Lochbihler; Joshua Schneider 001 (ITP, 2016)

A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks. - Andreas Lochbihler (Arch. Formal Proofs, 2016)

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. - Jasmin Christian Blanchette; Aymeric Bouzy; Andreas Lochbihler; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

CryptHOL. - Andreas Lochbihler (Arch. Formal Proofs, 2017)

Effect polymorphism in higher-order logic. - Andreas Lochbihler (Arch. Formal Proofs, 2017)

Probabilistic while loop. - Andreas Lochbihler (Arch. Formal Proofs, 2017)

Game-based cryptography in HOL. - Andreas Lochbihler; S. Reza Sefidgar; Bhargav Bhatt (Arch. Formal Proofs, 2017)

Monad normalisation. - Joshua Schneider 001; Manuel Eberl; Andreas Lochbihler (Arch. Formal Proofs, 2017)

Fast Machine Words in Isabelle/HOL. - Andreas Lochbihler (ITP, 2018)

Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. - Andreas Lochbihler; Joshua Schneider 001 (ITP, 2018)

Bounded Natural Functors with Covariance and Contravariance. - Andreas Lochbihler; Joshua Schneider 001 (Arch. Formal Proofs, 2018)

Constructive Cryptography in HOL. - Andreas Lochbihler; S. Reza Sefidgar (Arch. Formal Proofs, 2018)

A tutorial introduction to CryptHOL. - Andreas Lochbihler; S. Reza Sefidgar (IACR Cryptol. ePrint Arch., 2018)

Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler. - Andreas Lochbihler (J. Autom. Reason., 2018)

Formalizing Constructive Cryptography using CryptHOL. - Andreas Lochbihler; S. Reza Sefidgar; David A. Basin; Ueli Maurer (CSF, 2019)

Sigma Protocols and Commitment Schemes. - David Butler 002; Andreas Lochbihler (Arch. Formal Proofs, 2019)

Formalising Σ-Protocols and Commitment Schemes using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (IACR Cryptol. ePrint Arch., 2019)

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. - Peter Lammich; Andreas Lochbihler (J. Autom. Reason., 2019)

Effect Polymorphism in Higher-Order Logic (Proof Pearl). - Andreas Lochbihler (J. Autom. Reason., 2019)

Cardinality Estimators do not Preserve Privacy. - Damien Desfontaines; Andreas Lochbihler; David A. Basin (Proc. Priv. Enhancing Technol., 2019)

Authenticated Data Structures as Functors in Isabelle/HOL. - Andreas Lochbihler; Ognjen Maric (FMBC@CAV, 2020)

Authenticated Data Structures As Functors. - Andreas Lochbihler; Ognjen Maric (Arch. Formal Proofs, 2020)

CryptHOL: Game-Based Proofs in Higher-Order Logic. - David A. Basin; Andreas Lochbihler; S. Reza Sefidgar (J. Cryptol., 2020)

Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. - David A. Basin; Andreas Lochbihler; Ueli Maurer; S. Reza Sefidgar (CSF, 2021)

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. - Andreas Lochbihler (ITP, 2021)

Constructive Cryptography in HOL: the Communication Modeling Aspect. - Andreas Lochbihler; S. Reza Sefidgar (Arch. Formal Proofs, 2021)

Formalising $ varSigma$-Protocols and Commitment Schemes Using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (J. Autom. Reason., 2021)

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory. - Andreas Lochbihler (J. Autom. Reason., 2022)

Quotients of Bounded Natural Functors. - Basil Fürer; Andreas Lochbihler; Joshua Schneider 001; Dmitriy Traytel (Log. Methods Comput. Sci., 2022)

Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows. - Alexander Bernauer; Sofia Faro; Rémy Haemmerle; Martin Huschenbett; Moritz Kiefer; Andreas Lochbihler; Jussi Mäki; Francesco Mazzoli; Simon Meier; Neil Mitchell; Ratko G. Veprek (CoRR, 2023)