default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndreas Lochbihler
Person information
- affiliation: ETH Zurich, Switzerland
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[i7]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:
Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows. CoRR abs/2303.03749 (2023)- 2022
- [j33]Andreas Lochbihler
:
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory. J. Autom. Reason. 66(4): 585-610 (2022) - [j32]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. Log. Methods Comput. Sci. 18(1) (2022) - 2021
- [j31]Andreas Lochbihler, S. Reza Sefidgar:
Constructive Cryptography in HOL: the Communication Modeling Aspect. Arch. Formal Proofs 2021 (2021) - [j30]David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón:
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL. J. Autom. Reason. 65(4): 521-567 (2021) - [c25]David A. Basin, Andreas Lochbihler, Ueli Maurer, S. Reza Sefidgar:
Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. CSF 2021: 1-16 - [c24]Andreas Lochbihler:
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. ITP 2021: 25:1-25:18 - [i6]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. CoRR abs/2104.05348 (2021) - 2020
- [j29]Andreas Lochbihler, Ognjen Maric:
Authenticated Data Structures As Functors. Arch. Formal Proofs 2020 (2020) - [j28]David A. Basin, Andreas Lochbihler, S. Reza Sefidgar:
CryptHOL: Game-Based Proofs in Higher-Order Logic. J. Cryptol. 33(2): 494-566 (2020) - [c23]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. IJCAR (2) 2020: 58-78 - [c22]Andreas Lochbihler, Ognjen Maric:
Authenticated Data Structures as Functors in Isabelle/HOL. FMBC@CAV 2020: 6:1-6:15
2010 – 2019
- 2019
- [j27]David Butler, Andreas Lochbihler:
Sigma Protocols and Commitment Schemes. Arch. Formal Proofs 2019 (2019) - [j26]Peter Lammich, Andreas Lochbihler:
Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. J. Autom. Reason. 63(1): 53-94 (2019) - [j25]Andreas Lochbihler:
Effect Polymorphism in Higher-Order Logic (Proof Pearl). J. Autom. Reason. 63(2): 439-462 (2019) - [j24]Damien Desfontaines, Andreas Lochbihler, David A. Basin:
Cardinality Estimators do not Preserve Privacy. Proc. Priv. Enhancing Technol. 2019(2): 26-46 (2019) - [c21]Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, Ueli Maurer:
Formalizing Constructive Cryptography using CryptHOL. CSF 2019: 152-166 - [i5]David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón:
Formalising Σ-Protocols and Commitment Schemes using CryptHOL. IACR Cryptol. ePrint Arch. 2019: 1185 (2019) - 2018
- [j23]Andreas Lochbihler, Joshua Schneider:
Bounded Natural Functors with Covariance and Contravariance. Arch. Formal Proofs 2018 (2018) - [j22]Andreas Lochbihler, S. Reza Sefidgar:
Constructive Cryptography in HOL. Arch. Formal Proofs 2018 (2018) - [j21]Andreas Lochbihler:
Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler. J. Autom. Reason. 61(1-4): 243-332 (2018) - [c20]Andreas Lochbihler:
Fast Machine Words in Isabelle/HOL. ITP 2018: 388-410 - [c19]Andreas Lochbihler, Joshua Schneider:
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. ITP 2018: 411-431 - [i4]Damien Desfontaines, Andreas Lochbihler, David A. Basin:
Cardinality Estimators do not Preserve Privacy. CoRR abs/1808.05879 (2018) - [i3]Andreas Lochbihler, S. Reza Sefidgar:
A tutorial introduction to CryptHOL. IACR Cryptol. ePrint Arch. 2018: 941 (2018) - 2017
- [j20]Andreas Lochbihler:
CryptHOL. Arch. Formal Proofs 2017 (2017) - [j19]Andreas Lochbihler:
Effect polymorphism in higher-order logic. Arch. Formal Proofs 2017 (2017) - [j18]Andreas Lochbihler:
Probabilistic while loop. Arch. Formal Proofs 2017 (2017) - [j17]Andreas Lochbihler, S. Reza Sefidgar, Bhargav Bhatt:
Game-based cryptography in HOL. Arch. Formal Proofs 2017 (2017) - [j16]Joshua Schneider, Manuel Eberl, Andreas Lochbihler:
Monad normalisation. Arch. Formal Proofs 2017 (2017) - [c18]Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel:
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP 2017: 111-140 - [c17]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:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21 - [c16]Andreas Lochbihler:
Effect Polymorphism in Higher-Order Logic (Proof Pearl). ITP 2017: 389-409 - [i2]David A. Basin, Andreas Lochbihler, S. Reza Sefidgar:
CryptHOL: Game-based Proofs in Higher-order Logic. IACR Cryptol. ePrint Arch. 2017: 753 (2017) - 2016
- [j15]Andreas Lochbihler:
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks. Arch. Formal Proofs 2016 (2016) - [c15]Andreas Lochbihler:
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. ESOP 2016: 503-531 - [c14]Andreas Lochbihler, Joshua Schneider:
Equational Reasoning with Applicative Functors. ITP 2016: 252-273 - 2015
- [j14]Peter Gammie, Andreas Lochbihler:
The Stern-Brocot Tree. Arch. Formal Proofs 2015 (2015) - [j13]Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel:
A Zoo of Probabilistic Systems. Arch. Formal Proofs 2015 (2015) - [j12]Andreas Lochbihler, Tobias Nipkow:
Trie. Arch. Formal Proofs 2015 (2015) - [j11]Andreas Lochbihler, Joshua Schneider:
Applicative Lifting. Arch. Formal Proofs 2015 (2015) - [c13]Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel:
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP 2015: 203-220 - [c12]Andreas Lochbihler, Alexandra Maximova:
Stream Fusion for Isabelle's Code Generator - Rough Diamond. ITP 2015: 270-277 - 2014
- [j10]Andreas Lochbihler, Alexandra Maximova:
Stream Fusion in HOL with Code Generation. Arch. Formal Proofs 2014 (2014) - [j9]Andreas Lochbihler:
Analysing Java's safety guarantees under concurrency. it Inf. Technol. 56(2): 82-86 (2014) - [c11]Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014: 93-110 - [c10]Andreas Lochbihler, Johannes Hölzl:
Recursive Functions on Lazy Lists via Domains and Topologies. ITP 2014: 341-357 - 2013
- [j8]Andreas Lochbihler:
Light-weight Containers. Arch. Formal Proofs 2013 (2013) - [j7]Andreas Lochbihler:
Native Word. Arch. Formal Proofs 2013 (2013) - [j6]Andreas Lochbihler:
Making the java memory model safe. ACM Trans. Program. Lang. Syst. 35(4): 12:1-12:65 (2013) - [c9]Andreas Lochbihler:
Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. ITP 2013: 116-132 - 2012
- [b1]Andreas Lochbihler:
A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Karlsruhe Institute of Technology, KIT Scientific Publ. 2012, ISBN 978-3-86644-885-8, pp. 1-412 - [c8]Andreas Lochbihler:
Java and the Java Memory Model - A Unified, Machine-Checked Formalisation. ESOP 2012: 497-517 - [p1]Andreas Lochbihler:
Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. Ausgezeichnete Informatikdissertationen 2012: 211-220 - 2011
- [c7]Andreas Lochbihler, Lukas Bulwahn:
Animating the Formalised Semantics of a Java-Like Language. ITP 2011: 216-232 - 2010
- [j5]Andreas Lochbihler:
Coinductive. Arch. Formal Proofs 2010 (2010) - [c6]Andreas Lochbihler:
Verifying a Compiler for Java Threads. ESOP 2010: 427-447 - [c5]Peter Lammich, Andreas Lochbihler:
The Isabelle Collections Framework. ITP 2010: 339-354 - [c4]Bastian Katz, Marcus Krug, Andreas Lochbihler, Ignaz Rutter, Gregor Snelting, Dorothea Wagner:
Gateway Decompositions for Constrained Reachability Problems. SEA 2010: 449-461
2000 – 2009
- 2009
- [j4]Andreas Lochbihler:
Code Generation for Functions as Data. Arch. Formal Proofs 2009 (2009) - [j3]Andreas Lochbihler, Gregor Snelting:
On temporal path conditions in dependence graphs. Autom. Softw. Eng. 16(2): 263-290 (2009) - [c3]Andreas Lochbihler:
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009: 310-326 - 2008
- [j2]Kousha Etessami, Andreas Lochbihler:
The computational complexity of evolutionarily stable strategies. Int. J. Game Theory 37(1): 93-113 (2008) - [c2]Daniel Wasserrab, Andreas Lochbihler:
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLs 2008: 294-309 - 2007
- [j1]Andreas Lochbihler:
Jinja with Threads. Arch. Formal Proofs 2007 (2007) - [c1]Andreas Lochbihler, Gregor Snelting:
On Temporal Path Conditions in Dependence Graphs. SCAM 2007: 49-58 - 2004
- [i1]Kousha Etessami, Andreas Lochbihler:
The computational complexity of Evolutionarily Stable Strategies. Electron. Colloquium Comput. Complex. TR04 (2004)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
