Andreas Lochbihler

Orcid: 0000-0002-5851-494X

Affiliations:
  • ETH Zurich, Switzerland


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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows.
CoRR, 2023

2022
Quotients of Bounded Natural Functors.
Log. Methods Comput. Sci., 2022

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

2021
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL.
J. Autom. Reason., 2021

Constructive Cryptography in HOL: the Communication Modeling Aspect.
Arch. Formal Proofs, 2021

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks.
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL.
Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020
CryptHOL: Game-Based Proofs in Higher-Order Logic.
J. Cryptol., 2020

Authenticated Data Structures As Functors.
Arch. Formal Proofs, 2020

Authenticated Data Structures as Functors in Isabelle/HOL.
Proceedings of the 2nd Workshop on Formal Methods for Blockchains, 2020

2019
Cardinality Estimators do not Preserve Privacy.
Proc. Priv. Enhancing Technol., 2019

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

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches.
J. Autom. Reason., 2019

Formalising Σ-Protocols and Commitment Schemes using CryptHOL.
IACR Cryptol. ePrint Arch., 2019

Sigma Protocols and Commitment Schemes.
Arch. Formal Proofs, 2019

Formalizing Constructive Cryptography using CryptHOL.
Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

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

A tutorial introduction to CryptHOL.
IACR Cryptol. ePrint Arch., 2018

Constructive Cryptography in HOL.
Arch. Formal Proofs, 2018

Bounded Natural Functors with Covariance and Contravariance.
Arch. Formal Proofs, 2018

Relational Parametricity and Quotient Preservation for Modular (Co)datatypes.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Fast Machine Words in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017
Monad normalisation.
Arch. Formal Proofs, 2017

Game-based cryptography in HOL.
Arch. Formal Proofs, 2017

Probabilistic while loop.
Arch. Formal Proofs, 2017

Effect polymorphism in higher-order logic.
Arch. Formal Proofs, 2017

CryptHOL.
Arch. Formal Proofs, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.
Proceedings of the Programming Languages and Systems, 2017

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

Equational Reasoning with Applicative Functors.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Probabilistic Functions and Cryptographic Oracles in Higher Order Logic.
Proceedings of the Programming Languages and Systems, 2016

2015
Applicative Lifting.
Arch. Formal Proofs, 2015

Arch. Formal Proofs, 2015

A Zoo of Probabilistic Systems.
Arch. Formal Proofs, 2015

The Stern-Brocot Tree.
Arch. Formal Proofs, 2015

Stream Fusion for Isabelle's Code Generator - Rough Diamond.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014
Analysing Java's safety guarantees under concurrency.
it Inf. Technol., 2014

Stream Fusion in HOL with Code Generation.
Arch. Formal Proofs, 2014

Recursive Functions on Lazy Lists via Domains and Topologies.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
Making the java memory model safe.
ACM Trans. Program. Lang. Syst., 2013

Native Word.
Arch. Formal Proofs, 2013

Light-weight Containers.
Arch. Formal Proofs, 2013

Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable.
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.
PhD thesis, 2012

Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler.
Proceedings of the Ausgezeichnete Informatikdissertationen 2012, 2012

Java and the Java Memory Model - A Unified, Machine-Checked Formalisation.
Proceedings of the Programming Languages and Systems, 2012

2011
Animating the Formalised Semantics of a Java-Like Language.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010
Coinductive.
Arch. Formal Proofs, 2010

Gateway Decompositions for Constrained Reachability Problems.
Proceedings of the Experimental Algorithms, 9th International Symposium, 2010

The Isabelle Collections Framework.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Verifying a Compiler for Java Threads.
Proceedings of the Programming Languages and Systems, 2010

2009
On temporal path conditions in dependence graphs.
Autom. Softw. Eng., 2009

Code Generation for Functions as Data.
Arch. Formal Proofs, 2009

Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2008
The computational complexity of evolutionarily stable strategies.
Int. J. Game Theory, 2008

Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007
Jinja with Threads.
Arch. Formal Proofs, 2007


  Loading...