Andreas Lochbihler

According to our database, Andreas Lochbihler authored at least 60 papers between 2007 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

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

2022

Quotients of Bounded Natural Functors.

Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel

Log. Methods Comput. Sci., 2022

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory.

Andreas Lochbihler

J. Autom. Reason., 2022

2021

Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL.

David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón

J. Autom. Reason., 2021

Constructive Cryptography in HOL: the Communication Modeling Aspect.

Andreas Lochbihler, S. Reza Sefidgar

Arch. Formal Proofs, 2021

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks.

Andreas Lochbihler

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL.

David A. Basin, Andreas Lochbihler, Ueli Maurer, S. Reza Sefidgar

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

CryptHOL: Game-Based Proofs in Higher-Order Logic.

David A. Basin, Andreas Lochbihler, S. Reza Sefidgar

J. Cryptol., 2020

Authenticated Data Structures As Functors.

Andreas Lochbihler, Ognjen Maric

Arch. Formal Proofs, 2020

Authenticated Data Structures as Functors in Isabelle/HOL.

Andreas Lochbihler, Ognjen Maric

Proceedings of the 2nd Workshop on Formal Methods for Blockchains, 2020

2019

Cardinality Estimators do not Preserve Privacy.

Damien Desfontaines, Andreas Lochbihler, David A. Basin

Proc. Priv. Enhancing Technol., 2019

Effect Polymorphism in Higher-Order Logic (Proof Pearl).

Andreas Lochbihler

J. Autom. Reason., 2019

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches.

Peter Lammich, Andreas Lochbihler

J. Autom. Reason., 2019

Formalising Σ-Protocols and Commitment Schemes using CryptHOL.

David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón

IACR Cryptol. ePrint Arch., 2019

Sigma Protocols and Commitment Schemes.

David Butler, Andreas Lochbihler

Arch. Formal Proofs, 2019

Formalizing Constructive Cryptography using CryptHOL.

Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, Ueli Maurer

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

2018

Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler.

Andreas Lochbihler

J. Autom. Reason., 2018

A tutorial introduction to CryptHOL.

Andreas Lochbihler, S. Reza Sefidgar

IACR Cryptol. ePrint Arch., 2018

Constructive Cryptography in HOL.

Andreas Lochbihler, S. Reza Sefidgar

Arch. Formal Proofs, 2018

Bounded Natural Functors with Covariance and Contravariance.

Andreas Lochbihler, Joshua Schneider

Arch. Formal Proofs, 2018

Relational Parametricity and Quotient Preservation for Modular (Co)datatypes.

Andreas Lochbihler, Joshua Schneider

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Fast Machine Words in Isabelle/HOL.

Andreas Lochbihler

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Monad normalisation.

Joshua Schneider, Manuel Eberl, Andreas Lochbihler

Arch. Formal Proofs, 2017

Game-based cryptography in HOL.

Andreas Lochbihler, S. Reza Sefidgar, Bhargav Bhatt

Arch. Formal Proofs, 2017

Probabilistic while loop.

Andreas Lochbihler

Arch. Formal Proofs, 2017

Effect polymorphism in higher-order logic.

Andreas Lochbihler

Arch. Formal Proofs, 2017

CryptHOL.

Andreas Lochbihler

Arch. Formal Proofs, 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, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

Proceedings of the Programming Languages and Systems, 2017

2016

A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks.

Andreas Lochbihler

Arch. Formal Proofs, 2016

Equational Reasoning with Applicative Functors.

Andreas Lochbihler, Joshua Schneider

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Probabilistic Functions and Cryptographic Oracles in Higher Order Logic.

Andreas Lochbihler

Proceedings of the Programming Languages and Systems, 2016

2015

Applicative Lifting.

Andreas Lochbihler, Joshua Schneider

Arch. Formal Proofs, 2015

Trie.

Andreas Lochbihler, Tobias Nipkow

Arch. Formal Proofs, 2015

A Zoo of Probabilistic Systems.

Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel

Arch. Formal Proofs, 2015

The Stern-Brocot Tree.

Peter Gammie, Andreas Lochbihler

Arch. Formal Proofs, 2015

Stream Fusion for Isabelle's Code Generator - Rough Diamond.

Andreas Lochbihler, Alexandra Maximova

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl.

Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Analysing Java's safety guarantees under concurrency.

Andreas Lochbihler

it Inf. Technol., 2014

Stream Fusion in HOL with Code Generation.

Andreas Lochbihler, Alexandra Maximova

Arch. Formal Proofs, 2014

Recursive Functions on Lazy Lists via Domains and Topologies.

Andreas Lochbihler, Johannes Hölzl

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.

Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Making the java memory model safe.

Andreas Lochbihler

ACM Trans. Program. Lang. Syst., 2013

Native Word.

Andreas Lochbihler

Arch. Formal Proofs, 2013

Light-weight Containers.

Andreas Lochbihler

Arch. Formal Proofs, 2013

Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable.

Andreas Lochbihler

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler.

Andreas Lochbihler

PhD thesis, 2012

Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler.

Andreas Lochbihler

Proceedings of the Ausgezeichnete Informatikdissertationen 2012, 2012

Java and the Java Memory Model - A Unified, Machine-Checked Formalisation.

Andreas Lochbihler

Proceedings of the Programming Languages and Systems, 2012

2011

Animating the Formalised Semantics of a Java-Like Language.

Andreas Lochbihler, Lukas Bulwahn

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

Coinductive.

Andreas Lochbihler

Arch. Formal Proofs, 2010

Gateway Decompositions for Constrained Reachability Problems.

Bastian Katz, Marcus Krug, Andreas Lochbihler, Ignaz Rutter, Gregor Snelting, Dorothea Wagner

Proceedings of the Experimental Algorithms, 9th International Symposium, 2010

The Isabelle Collections Framework.

Peter Lammich, Andreas Lochbihler

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Verifying a Compiler for Java Threads.

Andreas Lochbihler

Proceedings of the Programming Languages and Systems, 2010

2009

On temporal path conditions in dependence graphs.

Andreas Lochbihler, Gregor Snelting

Autom. Softw. Eng., 2009

Code Generation for Functions as Data.

Andreas Lochbihler

Arch. Formal Proofs, 2009

Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL.

Andreas Lochbihler

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2008

The computational complexity of evolutionarily stable strategies.

Kousha Etessami, Andreas Lochbihler

Int. J. Game Theory, 2008

Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL.

Daniel Wasserrab, Andreas Lochbihler

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007

Jinja with Threads.

Andreas Lochbihler

Arch. Formal Proofs, 2007