Edit Profile (opens in new tab) Lochbihler, Andreas Compute Distance To: Compute Author ID: lochbihler.andreas Published as: Lochbihler, Andreas; Lochbihler, A. Documents Indexed: 27 Publications since 2008 Co-Authors: 24 Co-Authors with 17 Joint Publications 347 Co-Co-Authors all top 5 Co-Authors 10 single-authored 6 Traytel, Dmitry 4 Hölzl, Johannes 4 Schneider, Joshua P. 3 Blanchette, Jasmin Christian 3 Popescu, Andrei 2 Bouzy, Aymeric 2 Fürer, Basil 2 Lammich, Peter 2 Panny, Lorenz 1 Aspinall, David 1 Basin, David A. 1 Biendarra, Julian 1 Bulwahn, Lukas 1 Desharnais, Martin 1 Etessami, Kousha 1 Fleury, Mathias 1 Gascón, Adrià 1 Kunčar, Ondřej 1 Maximova, Alexandra 1 Meier, Fabian 1 Sefidgar, S. Reza 1 Sternagel, Christian 1 Thiemann, René 1 Wasserrab, Daniel Serials 5 Journal of Automated Reasoning 1 International Journal of Game Theory 1 Journal of Cryptology 1 Logical Methods in Computer Science Fields 26 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 1 Category theory; homological algebra (18-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 21 Publications have been cited 135 times in 79 Documents Cited by ▼ Year ▼ Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Probabilistic functions and cryptographic oracles in higher order logic. Zbl 1335.68033Lochbihler, Andreas 11 2016 Java and the Java memory model – a unified, machine-checked formalisation. Zbl 1352.68034Lochbihler, Andreas 10 2012 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 Light-weight containers for Isabelle: efficient, extensible, nestable. Zbl 1317.68219Lochbihler, Andreas 9 2013 Verifying a compiler for Java threads. Zbl 1260.68080Lochbihler, Andreas 8 2010 The Isabelle collections framework. Zbl 1291.68357Lammich, Peter; Lochbihler, Andreas 8 2010 A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy 8 2015 The computational complexity of evolutionarily stable strategies. Zbl 1147.91005Etessami, K.; Lochbihler, A. 8 2008 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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 CryptHOL: game-based proofs in higher-order logic. Zbl 1455.94121Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza 4 2020 Equational reasoning with applicative functors. Zbl 1464.68063Lochbihler, Andreas; Schneider, Joshua 4 2016 Animating the formalised semantics of a Java-like language. Zbl 1342.68294Lochbihler, Andreas; Bulwahn, Lukas 4 2011 Formalising FinFuns – generating code for functions as data from Isabelle/HOL. Zbl 1252.68260Lochbihler, Andreas 3 2009 Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178Lochbihler, Andreas 3 2018 Fast machine words in Isabelle/HOL. Zbl 06946992Lochbihler, Andreas 3 2018 Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169Lochbihler, Andreas; Hölzl, Johannes 2 2014 Relational parametricity and quotient preservation for modular (co)datatypes. Zbl 06946993Lochbihler, Andreas; Schneider, Joshua 2 2018 Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062Lochbihler, Andreas 2 2019 Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228Lammich, Peter; Lochbihler, Andreas 2 2019 Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68061Lochbihler, Andreas 1 2017 CryptHOL: game-based proofs in higher-order logic. Zbl 1455.94121Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza 4 2020 Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062Lochbihler, Andreas 2 2019 Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228Lammich, Peter; Lochbihler, Andreas 2 2019 Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178Lochbihler, Andreas 3 2018 Fast machine words in Isabelle/HOL. Zbl 06946992Lochbihler, Andreas 3 2018 Relational parametricity and quotient preservation for modular (co)datatypes. Zbl 06946993Lochbihler, Andreas; Schneider, Joshua 2 2018 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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.68061Lochbihler, Andreas 1 2017 Probabilistic functions and cryptographic oracles in higher order logic. Zbl 1335.68033Lochbihler, Andreas 11 2016 Equational reasoning with applicative functors. Zbl 1464.68063Lochbihler, Andreas; Schneider, Joshua 4 2016 A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy 8 2015 Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169Lochbihler, Andreas; Hölzl, Johannes 2 2014 Light-weight containers for Isabelle: efficient, extensible, nestable. Zbl 1317.68219Lochbihler, Andreas 9 2013 Java and the Java memory model – a unified, machine-checked formalisation. Zbl 1352.68034Lochbihler, Andreas 10 2012 Animating the formalised semantics of a Java-like language. Zbl 1342.68294Lochbihler, Andreas; Bulwahn, Lukas 4 2011 Verifying a compiler for Java threads. Zbl 1260.68080Lochbihler, Andreas 8 2010 The Isabelle collections framework. Zbl 1291.68357Lammich, Peter; Lochbihler, Andreas 8 2010 Formalising FinFuns – generating code for functions as data from Isabelle/HOL. Zbl 1252.68260Lochbihler, Andreas 3 2009 The computational complexity of evolutionarily stable strategies. Zbl 1147.91005Etessami, K.; Lochbihler, A. 8 2008 all cited Publications top 5 cited Publications all top 5 Cited by 124 Authors 13 Lochbihler, Andreas 8 Blanchette, Jasmin Christian 7 Traytel, Dmitry 6 Nipkow, Tobias 6 Popescu, Andrei 5 Lammich, Peter 4 Schneider, Joshua P. 3 Divasón, Jose 3 Murray, Toby 2 Abel, Andreas M. 2 Aransay, Jesús 2 Basin, David A. 2 Bauereiß, Thomas 2 Brunner, Julian 2 Felgenhauer, Bertram 2 Fürer, Basil 2 Hansen, Kristoffer Arnsfelt 2 Hölzl, Johannes 2 Kunčar, Ondřej 2 Matichuk, Daniel 2 Momigliano, Alberto 2 Paulson, Lawrence Charles 2 Pesenti Gritti, Armando 2 Pientka, Brigitte 2 Pous, Damien 2 Raimondi, Franco 2 Reynolds, Andrew 2 Roßkopf, Simon 2 Schlichtkrull, Anders 2 Sison, Robert 2 Thiemann, René 2 Waldmann, Uwe 2 Wenzel, Makarius 1 Allais, Guillaume 1 Aspinall, David 1 Avigad, Jeremy 1 Basold, Henning 1 Berenbrink, Petra 1 Bertholon, Guillaume 1 Blanc, Manon 1 Bomze, Immanuel M. 1 Bouzy, Aymeric 1 Bro Miltersen, Peter 1 Bulwahn, Lukas 1 Caminati, Marco Bright 1 Cockx, Jesper 1 Cohen, Liron 1 Colvin, Robert J. 1 Conitzer, Vincent 1 Dardinier, Thibault 1 Eberl, Manuel 1 Echenim, Mnacho 1 Etessami, Kousha 1 Feng, Xinyu 1 Fleury, Mathias 1 Fu, Yu-Fu 1 Gammie, Peter 1 Gascón, Adrià 1 Gheri, Lorenzo 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 Johann, Patricia 1 Joosten, Sebastiaan J. C. 1 Kitagawa, Fuyuki 1 Krstić, Srđan 1 Kuncak, Viktor 1 Küster Filipe Bowles, Juliana 1 Lin, Shangwei 1 Liu, Jiaxiang 1 Liu, Yang 1 Lochmann, Alexander 1 Marmsoler, Diego 1 Martin-Dorel, Érik 1 Matsuda, Takahiro 1 Melissourgos, Themistoklis 1 Middeldorp, Aart 1 Minamide, Yasuhiko 1 Mitterwallner, Fabian 1 Moser, Georg 1 Peltier, Nicolas 1 Polonsky, Andrew 1 Raszyk, Martin 1 Robillard, Simon 1 Rota Bulò, Samuel 1 Roughgarden, Tim 1 Roux, Pierre 1 Sanán, David 1 Sangiorgi, Davide 1 Sato, Tetsuya 1 Schäfer, Steven ...and 24 more Authors all top 5 Cited in 13 Serials 22 Journal of Automated Reasoning 5 Formal Aspects of Computing 3 Journal of Functional Programming 2 Information and Computation 1 International Journal of Game Theory 1 Mathematics of Operations Research 1 Theoretical Computer Science 1 Journal of Cryptology 1 MSCS. Mathematical Structures in Computer Science 1 Games and Economic Behavior 1 Economic Theory 1 Logical Methods in Computer Science 1 Frontiers of Computer Science all top 5 Cited in 15 Fields 74 Computer science (68-XX) 14 Mathematical logic and foundations (03-XX) 9 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Information and communication theory, circuits (94-XX) 2 Combinatorics (05-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Operations research, mathematical programming (90-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Category theory; homological algebra (18-XX) 1 Convex and discrete geometry (52-XX) 1 Probability theory and stochastic processes (60-XX) 1 Numerical analysis (65-XX) 1 Biology and other natural sciences (92-XX) Citations by Year