×

Lochbihler, Andreas

Author ID: lochbihler.andreas Recent zbMATH articles by "Lochbihler, Andreas"
Published as: Lochbihler, Andreas; Lochbihler, A.
Documents Indexed: 28 Publications since 2008
Co-Authors: 24 Co-Authors with 17 Joint Publications
384 Co-Co-Authors

Publications by Year

Citations contained in zbMATH Open

24 Publications have been cited 170 times in 95 Documents Cited by Year
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
36
2014
Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280
Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy
13
2017
Probabilistic functions and cryptographic oracles in higher order logic. Zbl 1335.68033
Lochbihler, Andreas
13
2016
The Isabelle collections framework. Zbl 1291.68357
Lammich, Peter; Lochbihler, Andreas
13
2010
Light-weight containers for Isabelle: efficient, extensible, nestable. Zbl 1317.68219
Lochbihler, Andreas
11
2013
Java and the Java memory model – a unified, machine-checked formalisation. Zbl 1352.68034
Lochbihler, Andreas
11
2012
A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199
Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy
10
2015
Verifying a compiler for Java threads. Zbl 1260.68080
Lochbihler, Andreas
9
2010
The computational complexity of evolutionarily stable strategies. Zbl 1147.91005
Etessami, K.; Lochbihler, A.
8
2008
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
6
2017
Equational reasoning with applicative functors. Zbl 1464.68063
Lochbihler, Andreas; Schneider, Joshua
5
2016
CryptHOL: game-based proofs in higher-order logic. Zbl 1455.94121
Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza
5
2020
Animating the formalised semantics of a Java-like language. Zbl 1342.68294
Lochbihler, Andreas; Bulwahn, Lukas
4
2011
A mechanized proof of the max-flow min-cut theorem for countable networks. Zbl 07699442
Lochbihler, Andreas
4
2021
Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228
Lammich, Peter; Lochbihler, Andreas
3
2019
Formalising FinFuns – generating code for functions as data from Isabelle/HOL. Zbl 1252.68260
Lochbihler, Andreas
3
2009
Fast machine words in Isabelle/HOL. Zbl 1511.68324
Lochbihler, Andreas
3
2018
Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062
Lochbihler, Andreas
2
2019
Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169
Lochbihler, Andreas; Hölzl, Johannes
2
2014
Quotients of bounded natural functors. Zbl 07614662
Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy
2
2020
Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68061
Lochbihler, Andreas
2
2017
Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178
Lochbihler, Andreas
2
2018
Relational parametricity and quotient preservation for modular (co)datatypes. Zbl 1511.68174
Lochbihler, Andreas; Schneider, Joshua
2
2018
A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. Zbl 1512.05165
Lochbihler, Andreas
1
2022
A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. Zbl 1512.05165
Lochbihler, Andreas
1
2022
A mechanized proof of the max-flow min-cut theorem for countable networks. Zbl 07699442
Lochbihler, Andreas
4
2021
CryptHOL: game-based proofs in higher-order logic. Zbl 1455.94121
Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza
5
2020
Quotients of bounded natural functors. Zbl 07614662
Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy
2
2020
Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228
Lammich, Peter; Lochbihler, Andreas
3
2019
Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062
Lochbihler, Andreas
2
2019
Fast machine words in Isabelle/HOL. Zbl 1511.68324
Lochbihler, Andreas
3
2018
Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178
Lochbihler, Andreas
2
2018
Relational parametricity and quotient preservation for modular (co)datatypes. Zbl 1511.68174
Lochbihler, Andreas; Schneider, Joshua
2
2018
Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280
Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy
13
2017
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
6
2017
Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68061
Lochbihler, Andreas
2
2017
Probabilistic functions and cryptographic oracles in higher order logic. Zbl 1335.68033
Lochbihler, Andreas
13
2016
Equational reasoning with applicative functors. Zbl 1464.68063
Lochbihler, Andreas; Schneider, Joshua
5
2016
A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199
Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy
10
2015
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
36
2014
Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169
Lochbihler, Andreas; Hölzl, Johannes
2
2014
Light-weight containers for Isabelle: efficient, extensible, nestable. Zbl 1317.68219
Lochbihler, Andreas
11
2013
Java and the Java memory model – a unified, machine-checked formalisation. Zbl 1352.68034
Lochbihler, Andreas
11
2012
Animating the formalised semantics of a Java-like language. Zbl 1342.68294
Lochbihler, Andreas; Bulwahn, Lukas
4
2011
The Isabelle collections framework. Zbl 1291.68357
Lammich, Peter; Lochbihler, Andreas
13
2010
Verifying a compiler for Java threads. Zbl 1260.68080
Lochbihler, Andreas
9
2010
Formalising FinFuns – generating code for functions as data from Isabelle/HOL. Zbl 1252.68260
Lochbihler, Andreas
3
2009
The computational complexity of evolutionarily stable strategies. Zbl 1147.91005
Etessami, K.; Lochbihler, A.
8
2008
all top 5

Cited by 144 Authors

15 Lochbihler, Andreas
9 Blanchette, Jasmin Christian
8 Popescu, Andrei
8 Traytel, Dmitry
6 Lammich, Peter
6 Nipkow, Tobias
4 Divasón, Jose
4 Schneider, Joshua P.
3 Aransay, Jesús
3 Hölzl, Johannes
3 Kunčar, Ondřej
3 Paulson, Lawrence Charles
3 Thiemann, René
3 Waldmann, Uwe
2 Abel, Andreas M.
2 Aspinall, David
2 Basin, David A.
2 Bauereiß, Thomas
2 Brunner, Julian
2 Felgenhauer, Bertram
2 Fürer, Basil
2 Gascón, Adrià
2 Gheri, Lorenzo
2 Hansen, Kristoffer Arnsfelt
2 Matichuk, Daniel
2 Momigliano, Alberto
2 Murray, Toby
2 Pesenti Gritti, Armando
2 Pientka, Brigitte
2 Pous, Damien
2 Raimondi, Franco
2 Reynolds, Andrew
2 Robillard, Simon
2 Roßkopf, Simon
2 Schlichtkrull, Anders
2 Tourret, Sophie
2 Wenzel, Makarius
1 Allais, Guillaume
1 Åman Pohjola, Johannes
1 Avigad, Jeremy
1 Basold, Henning
1 Berenbrink, Petra
1 Bertholon, Guillaume
1 Blanc, Manon
1 Bomze, Immanuel M.
1 Bonchi, Filippo
1 Bouzy, Aymeric
1 Bro Miltersen, Peter
1 Broadbent, Anne
1 Bulwahn, Lukas
1 Caminati, Marco Bright
1 Chan, T.-H. Hubert
1 Cockx, Jesper
1 Cohen, Liron
1 Colvin, Robert J.
1 Conitzer, Vincent
1 Dardinier, Thibault
1 Diaz, Javier
1 Dupuis, Frédéric
1 Eberl, Manuel
1 Echenim, Mnacho
1 Einarsdóttir, Sólrún Halla
1 Etessami, Kousha
1 Feng, Xinyu
1 Fleuriot, Jacques D.
1 Fleury, Mathias
1 Fu, Yu-Fu
1 Gammie, Peter
1 Gidey, Habtom Kashay
1 Guiol, Hervé
1 Hameer, Aliya
1 Hanaoka, Goichiro
1 Haslbeck, Max W.
1 Haslbeck, Maximilian P. L.
1 Hayes, Ian J.
1 Heimes, Lukas
1 Hirata, Michikazu
1 Hou, Ping
1 Hudon, Simon
1 Hupel, Lars
1 Jeltsch, Wolfgang
1 Johann, Patricia
1 Johansson, Moa
1 Joosten, Sebastiaan J. C.
1 Karvonen, Martti
1 Kitagawa, Fuyuki
1 König, Barbara
1 Krstić, Srđan
1 Kuncak, Viktor
1 Küster Filipe Bowles, Juliana
1 Lewis, Robert Y.
1 Lin, Shangwei
1 Liu, Jiaxiang
1 Liu, Yang
1 Lochmann, Alexander
1 Macbeth, Heather R.
1 Maimon, Shir
1 Marmsoler, Diego
1 Martin-Dorel, Érik
1 Matsuda, Takahiro
...and 44 more Authors

Citations by Year