Andreas Lochbihler

67 papers A 6B 13C 1Journal 40Unranked 5

Year	Rank	Type	Title / Venue / Authors
2023	J	`jnl`	Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows. CoRR 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
2022	J	`jnl`	A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory. J. Autom. Reason. Andreas Lochbihler
2022	J	`jnl`	Quotients of Bounded Natural Functors. Log. Methods Comput. Sci. Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2021	B	`conf`	A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. ITP Andreas Lochbihler
2021	A	`conf`	Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. CSF David A. Basin, Andreas Lochbihler, Ueli Maurer, S. Reza Sefidgar
2021	J	`jnl`	Constructive Cryptography in HOL: the Communication Modeling Aspect. Arch. Formal Proofs Andreas Lochbihler, S. Reza Sefidgar
2021	J	`jnl`	Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL. J. Autom. Reason. David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón
2021	J	`jnl`	Quotients of Bounded Natural Functors. CoRR Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2020	J	`jnl`	Authenticated Data Structures As Functors. Arch. Formal Proofs Andreas Lochbihler, Ognjen Maric
2020	—	`conf`	Authenticated Data Structures as Functors in Isabelle/HOL. FMBC@CAV Andreas Lochbihler, Ognjen Maric
2020	J	`jnl`	CryptHOL: Game-Based Proofs in Higher-Order Logic. J. Cryptol. David A. Basin, Andreas Lochbihler, S. Reza Sefidgar
2020	—	`conf`	Quotients of Bounded Natural Functors. IJCAR (2) Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2019	J	`jnl`	Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. J. Autom. Reason. Peter Lammich, Andreas Lochbihler
2019	J	`jnl`	Cardinality Estimators do not Preserve Privacy. Proc. Priv. Enhancing Technol. Damien Desfontaines, Andreas Lochbihler, David A. Basin
2019	J	`jnl`	Effect Polymorphism in Higher-Order Logic (Proof Pearl). J. Autom. Reason. Andreas Lochbihler
2019	J	`jnl`	Formalising Σ-Protocols and Commitment Schemes using CryptHOL. IACR Cryptol. ePrint Arch. David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón
2019	A	`conf`	Formalizing Constructive Cryptography using CryptHOL. CSF Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, Ueli Maurer
2019	J	`jnl`	Sigma Protocols and Commitment Schemes. Arch. Formal Proofs David Butler, Andreas Lochbihler
2018	J	`jnl`	A tutorial introduction to CryptHOL. IACR Cryptol. ePrint Arch. Andreas Lochbihler, S. Reza Sefidgar
2018	J	`jnl`	Bounded Natural Functors with Covariance and Contravariance. Arch. Formal Proofs Andreas Lochbihler, Joshua Schneider
2018	J	`jnl`	Cardinality Estimators do not Preserve Privacy. CoRR Damien Desfontaines, Andreas Lochbihler, David A. Basin
2018	J	`jnl`	Constructive Cryptography in HOL. Arch. Formal Proofs Andreas Lochbihler, S. Reza Sefidgar
2018	B	`conf`	Fast Machine Words in Isabelle/HOL. ITP Andreas Lochbihler
2018	J	`jnl`	Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler. J. Autom. Reason. Andreas Lochbihler
2018	B	`conf`	Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. ITP Andreas Lochbihler, Joshua Schneider
2017	J	`jnl`	CryptHOL. Arch. Formal Proofs Andreas Lochbihler
2017	J	`jnl`	CryptHOL: Game-based Proofs in Higher-order Logic. IACR Cryptol. ePrint Arch. David A. Basin, Andreas Lochbihler, S. Reza Sefidgar
2017	B	`conf`	Effect Polymorphism in Higher-Order Logic (Proof Pearl). ITP Andreas Lochbihler
2017	J	`jnl`	Effect polymorphism in higher-order logic. Arch. Formal Proofs Andreas Lochbihler
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 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
2017	A	`conf`	Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
2017	J	`jnl`	Game-based cryptography in HOL. Arch. Formal Proofs Andreas Lochbihler, S. Reza Sefidgar, Bhargav Bhatt
2017	J	`jnl`	Monad normalisation. Arch. Formal Proofs Joshua Schneider, Manuel Eberl, Andreas Lochbihler
2017	J	`jnl`	Probabilistic while loop. Arch. Formal Proofs Andreas Lochbihler
2016	J	`jnl`	A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks. Arch. Formal Proofs Andreas Lochbihler
2016	B	`conf`	Equational Reasoning with Applicative Functors. ITP Andreas Lochbihler, Joshua Schneider
2016	A	`conf`	Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. ESOP Andreas Lochbihler
2015	B	`conf`	A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	J	`jnl`	A Zoo of Probabilistic Systems. Arch. Formal Proofs Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	J	`jnl`	Applicative Lifting. Arch. Formal Proofs Andreas Lochbihler, Joshua Schneider
2015	B	`conf`	Stream Fusion for Isabelle's Code Generator - Rough Diamond. ITP Andreas Lochbihler, Alexandra Maximova
2015	J	`jnl`	The Stern-Brocot Tree. Arch. Formal Proofs Peter Gammie, Andreas Lochbihler
2015	J	`jnl`	Trie. Arch. Formal Proofs Andreas Lochbihler, Tobias Nipkow
2014	J	`jnl`	Analysing Java's safety guarantees under concurrency. it Inf. Technol. Andreas Lochbihler
2014	B	`conf`	Recursive Functions on Lazy Lists via Domains and Topologies. ITP Andreas Lochbihler, Johannes Hölzl
2014	J	`jnl`	Stream Fusion in HOL with Code Generation. Arch. Formal Proofs Andreas Lochbihler, Alexandra Maximova
2014	B	`conf`	Truly Modular (Co)datatypes for Isabelle/HOL. ITP Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
2013	B	`conf`	Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. ITP Andreas Lochbihler
2013	J	`jnl`	Light-weight Containers. Arch. Formal Proofs Andreas Lochbihler
2013	J	`jnl`	Making the java memory model safe. ACM Trans. Program. Lang. Syst. Andreas Lochbihler
2013	J	`jnl`	Native Word. Arch. Formal Proofs Andreas Lochbihler
2012	—	`—`	A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Andreas Lochbihler
2012	—	`ch.`	Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. Ausgezeichnete Informatikdissertationen Andreas Lochbihler
2012	A	`conf`	Java and the Java Memory Model - A Unified, Machine-Checked Formalisation. ESOP Andreas Lochbihler
2011	B	`conf`	Animating the Formalised Semantics of a Java-Like Language. ITP Andreas Lochbihler, Lukas Bulwahn
2010	J	`jnl`	Coinductive. Arch. Formal Proofs Andreas Lochbihler
2010	B	`conf`	Gateway Decompositions for Constrained Reachability Problems. SEA Bastian Katz, Marcus Krug, Andreas Lochbihler, Ignaz Rutter, Gregor Snelting, Dorothea Wagner
2010	B	`conf`	The Isabelle Collections Framework. ITP Peter Lammich, Andreas Lochbihler
2010	A	`conf`	Verifying a Compiler for Java Threads. ESOP Andreas Lochbihler
2009	J	`jnl`	Code Generation for Functions as Data. Arch. Formal Proofs Andreas Lochbihler
2009	—	`conf`	Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs Andreas Lochbihler
2009	J	`jnl`	On temporal path conditions in dependence graphs. Autom. Softw. Eng. Andreas Lochbihler, Gregor Snelting
2008	—	`conf`	Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLs Daniel Wasserrab, Andreas Lochbihler
2008	J	`jnl`	The computational complexity of evolutionarily stable strategies. Int. J. Game Theory Kousha Etessami, Andreas Lochbihler
2007	J	`jnl`	Jinja with Threads. Arch. Formal Proofs Andreas Lochbihler
2007	C	`conf`	On Temporal Path Conditions in Dependence Graphs. SCAM Andreas Lochbihler, Gregor Snelting
2004	J	`jnl`	The computational complexity of Evolutionarily Stable Strategies Electron. Colloquium Comput. Complex. Kousha Etessami, Andreas Lochbihler