Edit Profile (opens in new tab) Hofmann, Martin (b. 1965 d. 2018) Co-Author Distance Author ID: hofmann.martin.1 Published as: Hofmann, Martin; Hofmann, M. Homepage: https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann External Links: MGP · Wikidata · dblp · GND · IdRef · theses.fr Documents Indexed: 86 Publications since 1995, including 2 Books 7 Contributions as Editor · 1 Further Contribution Biographic References: 4 Publications Co-Authors: 60 Co-Authors with 72 Joint Publications 1,506 Co-Co-Authors all top 5 Co-Authors 20 single-authored 8 Beringer, Lennart 6 Dal Lago, Ugo 5 Aspinall, David 5 Benton, Nick 5 Streicher, Thomas 4 Jost, Steffen 4 Loidl, Hans-Wolfgang 4 Nigam, Vivek 4 Pierce, Benjamin C. 3 Karbyshev, Aleksandr 3 Momigliano, Alberto 3 Moser, Georg 3 Rodriguez, Dulma 3 Schöpp, Ulrich 2 Aehlig, Klaus 2 Altenkirch, Thorsten 2 Bauer, Andrej 2 Bauer, Sabine 2 Coquand, Thierry 2 Curien, Pierre-Louis 2 Garner, Richard 2 Grabowski, Robert 2 Hoffmann, Jan-Philipp 2 Hötzel Escardó, Martín 2 Kennedy, Andrew J. 2 Lange, Martin 2 Ledent, Jérémy 2 Ramyaa, Ramyaa 2 Sannella, Donald T. 2 Scott, Philip J. 2 Seidl, Helmut 2 Wagner, Daniel 1 Aczel, Peter 1 Ahrens, Benedikt 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Barth, Stephan 1 Bellantoni, Stephen J. 1 Berger, Ulrich 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Campbell, Brian A. 1 Chen, Wei 1 Cohen, Cyril 1 Constable, Robert Lee 1 Dax, Christian 1 Dybjer, Peter 1 Erbatur, Serdar 1 Finster, Eric 1 Gabbay, Murdoch James 1 Gambino, Nicola 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Hammond, Kevin 1 Harper, Robert 1 Harzheim, Sven 1 Hasegawa, Masahito 1 Herbelin, Hugo 1 Hofstra, Pieter J. W. 1 Hou (Favonia), Kuen-Bang 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kock, Joachim 1 Konečný, Michal 1 Kraus, Nicolai 1 Leutgeb, Lorenz 1 Li, Nuo 1 Licata, Dan 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Nahas, Michael 1 Neukirchen, Christian 1 Obwaller, David 1 Palmgren, Erik 1 Pavlova, Mariela 1 Pavlović, Duško 1 Pelayo, Alvaro 1 Plotkin, Gordon D. 1 Polonsky, Andrew 1 Rauschmayer, Axel 1 Riehl, Emily 1 Rijke, Egbert 1 Rosolini, Giuseppe 1 Rueß, Harald 1 Schwichtenberg, Helmut 1 Scott, Dana Stewart 1 Shkaravska, Olha 1 Shulman, Michael A. 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 Spitters, Bas ...and 14 more Co-Authors all top 5 Serials 8 Theoretical Computer Science 5 MSCS. Mathematical Structures in Computer Science 4 Information and Computation 3 Lecture Notes in Computer Science 2 Journal of Functional Programming 2 Logical Methods in Computer Science 1 Acta Mechanica 1 The Journal of Symbolic Logic 1 Annals of Pure and Applied Logic 1 Archive for Mathematical Logic 1 Nordic Journal of Computing 1 The Bulletin of Symbolic Logic 1 Theory of Computing Systems 1 Fundamenta Informaticae 1 Computer Languages, Systems & Structures 1 ACM Transactions on Computational Logic 1 Electronic Notes in Theoretical Computer Science 1 Distinguished Dissertations all top 5 Fields 78 Computer science (68-XX) 44 Mathematical logic and foundations (03-XX) 9 Category theory; homological algebra (18-XX) 7 General and overarching topics; collections (00-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 1 Combinatorics (05-XX) 1 General algebraic systems (08-XX) 1 Algebraic topology (55-XX) 1 Mechanics of deformable solids (74-XX) 1 Optics, electromagnetic theory (78-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 73 Publications have been cited 614 times in 406 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 The groupoid interpretation of type theory. Zbl 0930.03089Hofmann, Martin; Streicher, Thomas 58 1998 Syntax and semantics of dependent types. Zbl 0919.68083Hofmann, Martin 50 1997 Static prediction of heap space usage for first-order functional programs. Zbl 1321.68180Hofmann, Martin; Jost, Steffen 38 2003 Linear types and non-size-increasing polynomial time computation. Zbl 1054.68065Hofmann, Martin 31 2003 Multivariate amortized resource analysis. Zbl 1284.68132Hoffmann, Jan; Aehlig, Klaus; Hofmann, Martin 29 2011 On the interpretation of type theory in locally Cartesian closed categories. Zbl 1044.03544Hofmann, Martin 27 1995 Safe recursion with higher types and BCK-algebra. Zbl 0959.68075Hofmann, Martin 22 2000 A proof system for the linear time \(\mu \)-calculus. Zbl 1163.03308Dax, Christian; Hofmann, Martin; Lange, Martin 17 2006 Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. Zbl 1260.68074Hoffmann, Jan; Hofmann, Martin 16 2010 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069Coquand, Thierry; Hofmann, Martin 13 1999 A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. Zbl 0908.03022Hofmann, Martin 13 1998 Extensional constructs in intensional type theory. Zbl 1411.03001Hofmann, Martin 12 1997 On behavioural abstraction and behavioural satisfaction in higher-order logic. Zbl 0874.68196Hofmann, Martin; Sannella, Donald 12 1996 Type-based amortised heap-space analysis. Zbl 1178.68143Hofmann, Martin; Jost, Steffen 11 2006 Nominal renaming sets. Zbl 1182.03065Gabbay, Murdoch J.; Hofmann, Martin 11 2008 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 11 2007 Static determination of quantitative resource usage for higher-order programs. Zbl 1312.68039Jost, Steffen; Hammond, Kevin; Loidl, Hans-Wolfgang; Hofmann, Martin 11 2010 Symmetric lenses. Zbl 1284.18009Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel 10 2011 The strength of non-size increasing computation. Zbl 1323.68213Hofmann, Martin 10 2002 Automatic certification of heap consumption. Zbl 1108.68374Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha 9 2005 Sound and complete axiomatisations of call-by-value control operators. Zbl 0846.68066Hofmann, Martin 9 1995 An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut 8 2004 Realizability models for BLL-like languages. Zbl 1047.03049Hofmann, M.; Scott, P. J. 8 2004 Finite dimensional vector spaces are complete for traced symmetric monoidal categories. Zbl 1134.18003Hasegawa, Masahito; Hofmann, Martin; Plotkin, Gordon 8 2008 Revisiting the categorical interpretation of dependent type theory. Zbl 1433.03029Curien, Pierre-Louis; Garner, Richard; Hofmann, Martin 8 2014 Quantitative models and implicit complexity. Zbl 1172.68477Dal Lago, Ugo; Hofmann, Martin 8 2005 Realizability models and implicit complexity. Zbl 1222.03065Dal Lago, Ugo; Hofmann, Martin 7 2011 On the non-sequential nature of the interval-domain model of real-number computation. Zbl 1067.68070Escardó, Martín; Hofmann, Martin; Streicher, Thomas 7 2004 A new “feasible” arithmetic. Zbl 1006.03035Bellantoni, Stephen; Hofmann, Martin 7 2002 Completeness of continuation models for \(\lambda_\mu\)-calculus. Zbl 1096.03011Hofmann, Martin; Streicher, Thomas 7 2002 Reading, writing and relations. Towards extensional semantics for effect analyses. Zbl 1168.68356Benton, Nick; Kennedy, Andrew; Hofmann, Martin; Beringer, Lennart 7 2006 Abstract effects and proof-relevant logical relations. Zbl 1284.68371Benton, Nick; Hofmann, Martin; Nigam, Vivek 7 2014 Categorical reconstruction of a reduction free normalization proof. Zbl 1502.03019Altenkirch, Thorsten; Hofmann, Martin; Streicher, Thomas 7 1995 A type system for bounded space and functional in-place update. Zbl 0971.68023Hofmann, Martin 6 2000 Conservativity of equality reflection over intensional type theory. Zbl 1434.03038Hofmann, Martin 6 1996 A type system for bounded space and functional in-place update. (Extended abstract). Zbl 0964.68027Hofmann, Martin 5 2000 Positive subtyping. Zbl 0853.68125Hofmann, Martin; Pierce, Benjamin C. 5 1996 Automatic type inference for amortised heap-space analysis. Zbl 1381.68041Hofmann, Martin; Rodriguez, Dulma 4 2013 On monadic parametricity of second-order functionals. Zbl 1260.68071Bauer, Andrej; Hofmann, Martin; Karbyshev, Aleksandr 4 2013 A simple model for quotient types. Zbl 1063.68602Hofmann, Martin 4 1995 Efficient type-checking for amortised heap-space analysis. Zbl 1257.68051Hofmann, Martin; Rodriguez, Dulma 4 2009 Bounded linear logic, revisited. Zbl 1211.03090Dal Lago, Ugo; Hofmann, Martin 4 2010 Abstract interpretation from Büchi automata. Zbl 1401.68162Hofmann, Martin; Chen, Wei 4 2014 Amortised resource analysis and typed polynomial interpretations. Zbl 1416.68093Hofmann, Martin; Moser, Georg 4 2014 Edit lenses. Zbl 1321.68154Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel 4 2012 A semantic proof of polytime soundness of light affine logic. Zbl 1205.68169Dal Lago, Ugo; Hofmann, Martin 4 2010 Bounded linear logic, revisited. Zbl 1211.03089Dal Lago, Ugo; Hofmann, Martin 3 2009 Verifying pointer and string analyses with region type systems. Zbl 1253.68092Beringer, Lennart; Grabowski, Robert; Hofmann, Martin 3 2010 A type system with usage aspects. Zbl 1142.68019Aspinall, David; Hofmann, Martin; Konečný, Michal 3 2008 A Cartesian-closed category for higher-order model checking. Zbl 1460.68061Hofmann, Martin; Ledent, Jérémy 3 2017 Decidable inequalities over infinite trees. Zbl 1415.68059Bauer, Sabine; Jost, Steffen; Hofmann, Martin 3 2018 Multivariate amortised resource analysis for term rewrite systems. Zbl 1367.68138Hofmann, Martin; Moser, Georg 3 2015 Semantics of linear/modal lambda calculus. Zbl 0965.68011Hofmann, Martin 2 1999 Implementing a program logic of objects in a higher-order logic theorem prover. Zbl 0974.68185Hofmann, Martin; Tang, Francis 2 2000 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Automata theory and logic. (Automatentheorie und Logik.) Zbl 1257.68003Hofmann, Martin; Lange, Martin 2 2011 Certification using the Mobius base logic. Zbl 1209.68121Beringer, Lennart; Hofmann, Martin; Pavlova, Mariela 2 2008 Pure pointer programs with iteration. Zbl 1351.68101Hofmann, Martin; Schöpp, Ulrich 2 2010 An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. Zbl 0931.03058Hofmann, Martin 2 1997 What is a pure functional? Zbl 1288.68037Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut 2 2010 Well-foundedness in realizability. Zbl 1112.03058Hofmann, M.; van Oosten, J.; Streicher, T. 2 2006 Foundations of software science and computational structures. 14th international conference, FOSSACS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Zbl 1213.68041 1 2011 Pure pointer programs and tree isomorphism. Zbl 1260.68099Hofmann, Martin; Ramyaa, Ramyaa; Schöpp, Ulrich 1 2013 Verifying a local generic solver in Coq. Zbl 1306.68029Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut 1 2010 A bytecode logic for JML and types. Zbl 1168.68357Beringer, Lennart; Hofmann, Martin 1 2006 Proof-relevant logical relations for name generation. Zbl 1459.68041Benton, Nick; Hofmann, Martin; Nigam, Vivek 1 2018 Verifying pointer and string analyses with region type systems. Zbl 1290.68034Beringer, Lennart; Grabowski, Robert; Hofmann, Martin 1 2013 Trustworthly global computing. 5th international symposium, TGC 2010, Munich, Germany, February 24–26, 2010. Revised selected papers. Zbl 1198.68071 1 2010 Decidable linear list constraints. Zbl 1403.68232Bauer, Sabine; Hofmann, Martin 1 2017 Type-based analysis of logarithmic amortised complexity. Zbl 1517.68070Hofmann, Martin; Leutgeb, Lorenz; Obwaller, David; Moser, Georg; Zuleger, Florian 1 2022 Certification for \(\mu \)-calculus with winning strategies. Zbl 1354.68174Hofmann, Martin; Neukirchen, Christian; Rueß, Harald 1 2016 Logical relations and nondeterminism. Zbl 1453.68048Hofmann, Martin 1 2015 Type-based analysis of logarithmic amortised complexity. Zbl 1517.68070Hofmann, Martin; Leutgeb, Lorenz; Obwaller, David; Moser, Georg; Zuleger, Florian 1 2022 Decidable inequalities over infinite trees. Zbl 1415.68059Bauer, Sabine; Jost, Steffen; Hofmann, Martin 3 2018 Proof-relevant logical relations for name generation. Zbl 1459.68041Benton, Nick; Hofmann, Martin; Nigam, Vivek 1 2018 A Cartesian-closed category for higher-order model checking. Zbl 1460.68061Hofmann, Martin; Ledent, Jérémy 3 2017 Decidable linear list constraints. Zbl 1403.68232Bauer, Sabine; Hofmann, Martin 1 2017 Certification for \(\mu \)-calculus with winning strategies. Zbl 1354.68174Hofmann, Martin; Neukirchen, Christian; Rueß, Harald 1 2016 Multivariate amortised resource analysis for term rewrite systems. Zbl 1367.68138Hofmann, Martin; Moser, Georg 3 2015 Logical relations and nondeterminism. Zbl 1453.68048Hofmann, Martin 1 2015 Revisiting the categorical interpretation of dependent type theory. Zbl 1433.03029Curien, Pierre-Louis; Garner, Richard; Hofmann, Martin 8 2014 Abstract effects and proof-relevant logical relations. Zbl 1284.68371Benton, Nick; Hofmann, Martin; Nigam, Vivek 7 2014 Abstract interpretation from Büchi automata. Zbl 1401.68162Hofmann, Martin; Chen, Wei 4 2014 Amortised resource analysis and typed polynomial interpretations. Zbl 1416.68093Hofmann, Martin; Moser, Georg 4 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Automatic type inference for amortised heap-space analysis. Zbl 1381.68041Hofmann, Martin; Rodriguez, Dulma 4 2013 On monadic parametricity of second-order functionals. Zbl 1260.68071Bauer, Andrej; Hofmann, Martin; Karbyshev, Aleksandr 4 2013 Pure pointer programs and tree isomorphism. Zbl 1260.68099Hofmann, Martin; Ramyaa, Ramyaa; Schöpp, Ulrich 1 2013 Verifying pointer and string analyses with region type systems. Zbl 1290.68034Beringer, Lennart; Grabowski, Robert; Hofmann, Martin 1 2013 Edit lenses. Zbl 1321.68154Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel 4 2012 Multivariate amortized resource analysis. Zbl 1284.68132Hoffmann, Jan; Aehlig, Klaus; Hofmann, Martin 29 2011 Symmetric lenses. Zbl 1284.18009Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel 10 2011 Realizability models and implicit complexity. Zbl 1222.03065Dal Lago, Ugo; Hofmann, Martin 7 2011 Automata theory and logic. (Automatentheorie und Logik.) Zbl 1257.68003Hofmann, Martin; Lange, Martin 2 2011 Foundations of software science and computational structures. 14th international conference, FOSSACS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Zbl 1213.68041 1 2011 Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. Zbl 1260.68074Hoffmann, Jan; Hofmann, Martin 16 2010 Static determination of quantitative resource usage for higher-order programs. Zbl 1312.68039Jost, Steffen; Hammond, Kevin; Loidl, Hans-Wolfgang; Hofmann, Martin 11 2010 Bounded linear logic, revisited. Zbl 1211.03090Dal Lago, Ugo; Hofmann, Martin 4 2010 A semantic proof of polytime soundness of light affine logic. Zbl 1205.68169Dal Lago, Ugo; Hofmann, Martin 4 2010 Verifying pointer and string analyses with region type systems. Zbl 1253.68092Beringer, Lennart; Grabowski, Robert; Hofmann, Martin 3 2010 Pure pointer programs with iteration. Zbl 1351.68101Hofmann, Martin; Schöpp, Ulrich 2 2010 What is a pure functional? Zbl 1288.68037Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut 2 2010 Verifying a local generic solver in Coq. Zbl 1306.68029Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut 1 2010 Trustworthly global computing. 5th international symposium, TGC 2010, Munich, Germany, February 24–26, 2010. Revised selected papers. Zbl 1198.68071 1 2010 Efficient type-checking for amortised heap-space analysis. Zbl 1257.68051Hofmann, Martin; Rodriguez, Dulma 4 2009 Bounded linear logic, revisited. Zbl 1211.03089Dal Lago, Ugo; Hofmann, Martin 3 2009 Nominal renaming sets. Zbl 1182.03065Gabbay, Murdoch J.; Hofmann, Martin 11 2008 Finite dimensional vector spaces are complete for traced symmetric monoidal categories. Zbl 1134.18003Hasegawa, Masahito; Hofmann, Martin; Plotkin, Gordon 8 2008 A type system with usage aspects. Zbl 1142.68019Aspinall, David; Hofmann, Martin; Konečný, Michal 3 2008 Certification using the Mobius base logic. Zbl 1209.68121Beringer, Lennart; Hofmann, Martin; Pavlova, Mariela 2 2008 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 11 2007 A proof system for the linear time \(\mu \)-calculus. Zbl 1163.03308Dax, Christian; Hofmann, Martin; Lange, Martin 17 2006 Type-based amortised heap-space analysis. Zbl 1178.68143Hofmann, Martin; Jost, Steffen 11 2006 Reading, writing and relations. Towards extensional semantics for effect analyses. Zbl 1168.68356Benton, Nick; Kennedy, Andrew; Hofmann, Martin; Beringer, Lennart 7 2006 Well-foundedness in realizability. Zbl 1112.03058Hofmann, M.; van Oosten, J.; Streicher, T. 2 2006 A bytecode logic for JML and types. Zbl 1168.68357Beringer, Lennart; Hofmann, Martin 1 2006 Automatic certification of heap consumption. Zbl 1108.68374Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha 9 2005 Quantitative models and implicit complexity. Zbl 1172.68477Dal Lago, Ugo; Hofmann, Martin 8 2005 An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut 8 2004 Realizability models for BLL-like languages. Zbl 1047.03049Hofmann, M.; Scott, P. J. 8 2004 On the non-sequential nature of the interval-domain model of real-number computation. Zbl 1067.68070Escardó, Martín; Hofmann, Martin; Streicher, Thomas 7 2004 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Static prediction of heap space usage for first-order functional programs. Zbl 1321.68180Hofmann, Martin; Jost, Steffen 38 2003 Linear types and non-size-increasing polynomial time computation. Zbl 1054.68065Hofmann, Martin 31 2003 The strength of non-size increasing computation. Zbl 1323.68213Hofmann, Martin 10 2002 A new “feasible” arithmetic. Zbl 1006.03035Bellantoni, Stephen; Hofmann, Martin 7 2002 Completeness of continuation models for \(\lambda_\mu\)-calculus. Zbl 1096.03011Hofmann, Martin; Streicher, Thomas 7 2002 Safe recursion with higher types and BCK-algebra. Zbl 0959.68075Hofmann, Martin 22 2000 A type system for bounded space and functional in-place update. Zbl 0971.68023Hofmann, Martin 6 2000 A type system for bounded space and functional in-place update. (Extended abstract). Zbl 0964.68027Hofmann, Martin 5 2000 Implementing a program logic of objects in a higher-order logic theorem prover. Zbl 0974.68185Hofmann, Martin; Tang, Francis 2 2000 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069Coquand, Thierry; Hofmann, Martin 13 1999 Semantics of linear/modal lambda calculus. Zbl 0965.68011Hofmann, Martin 2 1999 The groupoid interpretation of type theory. Zbl 0930.03089Hofmann, Martin; Streicher, Thomas 58 1998 A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. Zbl 0908.03022Hofmann, Martin 13 1998 Syntax and semantics of dependent types. Zbl 0919.68083Hofmann, Martin 50 1997 Extensional constructs in intensional type theory. Zbl 1411.03001Hofmann, Martin 12 1997 An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. Zbl 0931.03058Hofmann, Martin 2 1997 On behavioural abstraction and behavioural satisfaction in higher-order logic. Zbl 0874.68196Hofmann, Martin; Sannella, Donald 12 1996 Conservativity of equality reflection over intensional type theory. Zbl 1434.03038Hofmann, Martin 6 1996 Positive subtyping. Zbl 0853.68125Hofmann, Martin; Pierce, Benjamin C. 5 1996 On the interpretation of type theory in locally Cartesian closed categories. Zbl 1044.03544Hofmann, Martin 27 1995 Sound and complete axiomatisations of call-by-value control operators. Zbl 0846.68066Hofmann, Martin 9 1995 Categorical reconstruction of a reduction free normalization proof. Zbl 1502.03019Altenkirch, Thorsten; Hofmann, Martin; Streicher, Thomas 7 1995 A simple model for quotient types. Zbl 1063.68602Hofmann, Martin 4 1995 all cited Publications top 5 cited Publications all top 5 Cited by 544 Authors 22 Hofmann, Martin 15 Dal Lago, Ugo 11 Baillot, Patrick 10 Coquand, Thierry 8 Albert, Elvira 7 Dybjer, Peter 7 Hennicker, Rolf 7 Palmgren, Erik 6 Altenkirch, Thorsten 6 Awodey, Steve 6 Beringer, Lennart 6 Birkedal, Lars 6 Hötzel Escardó, Martín 6 Lumsdaine, Peter LeFanu 6 Sattler, Christian 5 Avigad, Jeremy 5 Genaim, Samir 5 Moser, Georg 5 Pitts, Andrew M. 5 Streicher, Thomas 5 Zhang, Yu 4 Ahrens, Benedikt 4 Berger, Ulrich 4 Bidoit, Michel 4 Gabbay, Murdoch James 4 Gambino, Nicola 4 Garner, Richard 4 Huber, Simon 4 Moerdijk, Ieke 4 Peña, Ricardo 4 Puebla, Germán 4 Schwichtenberg, Helmut 4 Van den Berg, Benno 4 Warren, Michael Alton 4 Zuleger, Florian 3 Angiuli, Carlo 3 Arenas, Puri 3 Ariola, Zena M. 3 Aspinall, David 3 de’Liguoro, Ugo 3 Emmenegger, Jacopo 3 Florido, Mário 3 Ghani, Neil 3 Ghyselen, Alexis 3 Giesl, Jürgen 3 Gratzer, Daniel 3 Hähnle, Reiner 3 Hainry, Emmanuel 3 Harper, Robert 3 Herbelin, Hugo 3 Hofstra, Pieter J. W. 3 Leutgeb, Lorenz 3 Mackie, Ian 3 Marcial-Romero, José Raymundo 3 Mazza, Damiano 3 McBride, Conor Thomas 3 McKinna, James 3 Møgelberg, Rasmus Ejlers 3 Montenegro, Manuel 3 Nipkow, Tobias 3 Nowak, David E. 3 Orton, Ian 3 Péchoux, Romain 3 Pientka, Brigitte 3 Plotkin, Gordon D. 3 Redmond, Brian F. 3 Rosolini, Giuseppe 3 Sannella, Donald T. 3 Segura, Clara 3 Seidl, Helmut 3 Spitters, Bas 3 Studer, Thomas 3 Tabareau, Nicolas 3 Uustalu, Tarmo 3 van der Weide, Niels 3 Veltri, Niccolò 3 Vogler, Ralf 3 Wirsing, Martin 2 Abel, Andreas M. 2 Abou-Saleh, Faris 2 Abramsky, Samson 2 Accattoli, Beniamino 2 Ahman, Danel 2 Allais, Guillaume 2 Alonderis, Romas 2 Alves, Sandra 2 Atkey, Robert 2 Aubert, Clément 2 Avanzini, Martin 2 Barbanera, Franco 2 Barthe, Gilles 2 Basold, Henning 2 Bellantoni, Stephen J. 2 Benton, Nick 2 Bezem, Marc 2 Bizjak, Aleš 2 Bonfante, Guillaume 2 Boulier, Simon 2 Brunel, Aloïs 2 Cantini, Andrea ...and 444 more Authors all top 5 Cited in 46 Serials 48 Theoretical Computer Science 26 MSCS. Mathematical Structures in Computer Science 23 Annals of Pure and Applied Logic 22 Information and Computation 16 Logical Methods in Computer Science 14 Journal of Automated Reasoning 13 Journal of Functional Programming 8 The Journal of Symbolic Logic 5 Journal of Pure and Applied Algebra 5 Archive for Mathematical Logic 5 The Journal of Logic and Algebraic Programming 4 The Bulletin of Symbolic Logic 4 ACM Transactions on Computational Logic 4 Journal of Applied Logic 4 Journal of Logical and Algebraic Methods in Programming 3 Studia Logica 3 Formal Aspects of Computing 3 Indagationes Mathematicae. New Series 3 Theory and Applications of Categories 3 Theory of Computing Systems 3 Higher-Order and Symbolic Computation 2 Synthese 2 Science of Computer Programming 2 Formal Methods in System Design 2 Theory and Practice of Logic Programming 2 Computer Languages, Systems & Structures 1 Information Processing Letters 1 Mathematical Proceedings of the Cambridge Philosophical Society 1 Journal of the London Mathematical Society. Second Series 1 Mathematische Annalen 1 Forum Mathematicum 1 Bulletin of the American Mathematical Society. New Series 1 Analele Științifice ale Universității Al. I. Cuza din Iași. Serie Nouă. Matematică 1 Annales de la Faculté des Sciences de Toulouse. Mathématiques. Série VI 1 Mathematical Logic Quarterly (MLQ) 1 Journal of the European Mathematical Society (JEMS) 1 RAIRO. Theoretical Informatics and Applications 1 Concurrency and Computation: Practice & Experience 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 Mediterranean Journal of Mathematics 1 Oberwolfach Reports 1 Logica Universalis 1 Journal of Homotopy and Related Structures 1 Forum of Mathematics, Sigma 1 Categories and General Algebraic Structures with Applications 1 Higher Structures all top 5 Cited in 21 Fields 275 Computer science (68-XX) 232 Mathematical logic and foundations (03-XX) 85 Category theory; homological algebra (18-XX) 31 Algebraic topology (55-XX) 9 Information and communication theory, circuits (94-XX) 5 Order, lattices, ordered algebraic structures (06-XX) 5 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 4 General and overarching topics; collections (00-XX) 4 Quantum theory (81-XX) 3 Operations research, mathematical programming (90-XX) 2 History and biography (01-XX) 2 Group theory and generalizations (20-XX) 2 General topology (54-XX) 1 General algebraic systems (08-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) 1 \(K\)-theory (19-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Functional analysis (46-XX) 1 Probability theory and stochastic processes (60-XX) 1 Statistics (62-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.