×

zbMATH — the first resource for mathematics

Hofmann, Martin

Compute Distance To:
Author ID: hofmann.martin.1 Recent zbMATH articles by "Hofmann, Martin"
Published as: Hofmann, Martin; Hofmann, M.
Homepage: https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann
External Links: Google Scholar · MGP · Wikidata · dblp · GND
Documents Indexed: 87 Publications since 1995, including 7 Books
Biographic References: 1 Publication

Publications by Year

Citations contained in zbMATH Open

61 Publications have been cited 400 times in 271 Documents Cited by Year
The groupoid interpretation of type theory. Zbl 0930.03089
Hofmann, Martin; Streicher, Thomas
38
1998
Syntax and semantics of dependent types. Zbl 0919.68083
Hofmann, Martin
31
1997
Static prediction of heap space usage for first-order functional programs. Zbl 1321.68180
Hofmann, Martin; Jost, Steffen
27
2003
Linear types and non-size-increasing polynomial time computation. Zbl 1054.68065
Hofmann, Martin
22
2003
On the interpretation of type theory in locally Cartesian closed categories. Zbl 1044.03544
Hofmann, Martin
20
1995
Safe recursion with higher types and BCK-algebra. Zbl 0959.68075
Hofmann, Martin
18
2000
Multivariate amortized resource analysis. Zbl 1284.68132
Hoffmann, Jan; Aehlig, Klaus; Hofmann, Martin
15
2011
A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069
Coquand, Thierry; Hofmann, Martin
12
1999
On behavioural abstraction and behavioural satisfaction in higher-order logic. Zbl 0874.68196
Hofmann, Martin; Sannella, Donald
11
1996
A proof system for the linear time \(\mu \)-calculus. Zbl 1163.03308
Dax, Christian; Hofmann, Martin; Lange, Martin
10
2006
A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. Zbl 0908.03022
Hofmann, Martin
10
1998
Type-based amortised heap-space analysis. Zbl 1178.68143
Hofmann, Martin; Jost, Steffen
9
2006
Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. Zbl 1260.68074
Hoffmann, Jan; Hofmann, Martin
8
2010
A program logic for resources. Zbl 1133.68010
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
8
2007
Nominal renaming sets. Zbl 1182.03065
Gabbay, Murdoch J.; Hofmann, Martin
8
2008
Sound and complete axiomatisations of call-by-value control operators. Zbl 0846.68066
Hofmann, Martin
8
1995
Automatic certification of heap consumption. Zbl 1108.68374
Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha
8
2005
Extensional constructs in intensional type theory. Zbl 1411.03001
Hofmann, Martin
7
1997
On the non-sequential nature of the interval-domain model of real-number computation. Zbl 1067.68070
Escardó, Martín; Hofmann, Martin; Streicher, Thomas
7
2004
The strength of non-size increasing computation. Zbl 1323.68213
Hofmann, Martin
7
2002
Reading, writing and relations. Towards extensional semantics for effect analyses. Zbl 1168.68356
Benton, Nick; Kennedy, Andrew; Hofmann, Martin; Beringer, Lennart
6
2006
Finite dimensional vector spaces are complete for traced symmetric monoidal categories. Zbl 1134.18003
Hasegawa, Masahito; Hofmann, Martin; Plotkin, Gordon
6
2008
Completeness of continuation models for \(\lambda_\mu\)-calculus. Zbl 1096.03011
Hofmann, Martin; Streicher, Thomas
6
2002
Quantitative models and implicit complexity. Zbl 1172.68477
Dal Lago, Ugo; Hofmann, Martin
6
2005
Static determination of quantitative resource usage for higher-order programs. Zbl 1312.68039
Jost, Steffen; Hammond, Kevin; Loidl, Hans-Wolfgang; Hofmann, Martin
6
2010
Realizability models for BLL-like languages. Zbl 1047.03049
Hofmann, M.; Scott, P. J.
5
2004
A new “feasible” arithmetic. Zbl 1006.03035
Bellantoni, Stephen; Hofmann, Martin
5
2002
An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036
Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut
4
2004
Positive subtyping. Zbl 0853.68125
Hofmann, Martin; Pierce, Benjamin C.
4
1996
A type system for bounded space and functional in-place update. Zbl 0971.68023
Hofmann, Martin
4
2000
Abstract effects and proof-relevant logical relations. Zbl 1284.68371
Benton, Nick; Hofmann, Martin; Nigam, Vivek
4
2014
Realizability models and implicit complexity. Zbl 1222.03065
Dal Lago, Ugo; Hofmann, Martin
4
2011
Conservativity of equality reflection over intensional type theory. Zbl 1434.03038
Hofmann, Martin
3
1996
Bounded linear logic, revisited. Zbl 1211.03089
Dal Lago, Ugo; Hofmann, Martin
3
2009
A type system with usage aspects. Zbl 1142.68019
Aspinall, David; Hofmann, Martin; Konečný, Michal
3
2008
A type system for bounded space and functional in-place update. (Extended abstract). Zbl 0964.68027
Hofmann, Martin
3
2000
Symmetric lenses. Zbl 1284.18009
Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel
3
2011
Amortised resource analysis and typed polynomial interpretations. Zbl 1416.68093
Hofmann, Martin; Moser, Georg
3
2014
Revisiting the categorical interpretation of dependent type theory. Zbl 1433.03029
Curien, Pierre-Louis; Garner, Richard; Hofmann, Martin
3
2014
On monadic parametricity of second-order functionals. Zbl 1260.68071
Bauer, Andrej; Hofmann, Martin; Karbyshev, Aleksandr
3
2013
Certification using the Mobius base logic. Zbl 1209.68121
Beringer, Lennart; Hofmann, Martin; Pavlova, Mariela
2
2008
A semantic proof of polytime soundness of light affine logic. Zbl 1205.68169
Dal Lago, Ugo; Hofmann, Martin
2
2010
What is a pure functional? Zbl 1288.68037
Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut
2
2010
Efficient type-checking for amortised heap-space analysis. Zbl 1257.68051
Hofmann, Martin; Rodriguez, Dulma
2
2009
A simple model for quotient types. Zbl 1063.68602
Hofmann, Martin
2
1995
Semantics of linear/modal lambda calculus. Zbl 0965.68011
Hofmann, Martin
2
1999
A program logic for resource verification. Zbl 1099.68584
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
2
2004
Implementing a program logic of objects in a higher-order logic theorem prover. Zbl 0974.68185
Hofmann, Martin; Tang, Francis
2
2000
Bounded linear logic, revisited. Zbl 1211.03090
Dal Lago, Ugo; Hofmann, Martin
2
2010
Verifying pointer and string analyses with region type systems. Zbl 1253.68092
Beringer, Lennart; Grabowski, Robert; Hofmann, Martin
2
2010
Automata theory and logic. (Automatentheorie und Logik.) Zbl 1257.68003
Hofmann, Martin; Lange, Martin
2
2011
Verifying a local generic solver in Coq. Zbl 1306.68029
Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut
1
2010
A bytecode logic for JML and types. Zbl 1168.68357
Beringer, Lennart; Hofmann, Martin
1
2006
An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. Zbl 0931.03058
Hofmann, Martin
1
1997
Automatic type inference for amortised heap-space analysis. Zbl 1381.68041
Hofmann, Martin; Rodriguez, Dulma
1
2013
Multivariate amortised resource analysis for term rewrite systems. Zbl 1367.68138
Hofmann, Martin; Moser, Georg
1
2015
Edit lenses. Zbl 1321.68154
Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel
1
2012
Pure pointer programs with iteration. Zbl 1351.68101
Hofmann, Martin; Schöpp, Ulrich
1
2010
Well-foundedness in realizability. Zbl 1112.03058
Hofmann, M.; van Oosten, J.; Streicher, T.
1
2006
Pure pointer programs and tree isomorphism. Zbl 1260.68099
Hofmann, Martin; Ramyaa, Ramyaa; Schöpp, Ulrich
1
2013
Abstract interpretation from Büchi automata. Zbl 1401.68162
Hofmann, Martin; Chen, Wei
1
2014
Multivariate amortised resource analysis for term rewrite systems. Zbl 1367.68138
Hofmann, Martin; Moser, Georg
1
2015
Abstract effects and proof-relevant logical relations. Zbl 1284.68371
Benton, Nick; Hofmann, Martin; Nigam, Vivek
4
2014
Amortised resource analysis and typed polynomial interpretations. Zbl 1416.68093
Hofmann, Martin; Moser, Georg
3
2014
Revisiting the categorical interpretation of dependent type theory. Zbl 1433.03029
Curien, Pierre-Louis; Garner, Richard; Hofmann, Martin
3
2014
Abstract interpretation from Büchi automata. Zbl 1401.68162
Hofmann, Martin; Chen, Wei
1
2014
On monadic parametricity of second-order functionals. Zbl 1260.68071
Bauer, Andrej; Hofmann, Martin; Karbyshev, Aleksandr
3
2013
Automatic type inference for amortised heap-space analysis. Zbl 1381.68041
Hofmann, Martin; Rodriguez, Dulma
1
2013
Pure pointer programs and tree isomorphism. Zbl 1260.68099
Hofmann, Martin; Ramyaa, Ramyaa; Schöpp, Ulrich
1
2013
Edit lenses. Zbl 1321.68154
Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel
1
2012
Multivariate amortized resource analysis. Zbl 1284.68132
Hoffmann, Jan; Aehlig, Klaus; Hofmann, Martin
15
2011
Realizability models and implicit complexity. Zbl 1222.03065
Dal Lago, Ugo; Hofmann, Martin
4
2011
Symmetric lenses. Zbl 1284.18009
Hofmann, Martin; Pierce, Benjamin; Wagner, Daniel
3
2011
Automata theory and logic. (Automatentheorie und Logik.) Zbl 1257.68003
Hofmann, Martin; Lange, Martin
2
2011
Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. Zbl 1260.68074
Hoffmann, Jan; Hofmann, Martin
8
2010
Static determination of quantitative resource usage for higher-order programs. Zbl 1312.68039
Jost, Steffen; Hammond, Kevin; Loidl, Hans-Wolfgang; Hofmann, Martin
6
2010
A semantic proof of polytime soundness of light affine logic. Zbl 1205.68169
Dal Lago, Ugo; Hofmann, Martin
2
2010
What is a pure functional? Zbl 1288.68037
Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut
2
2010
Bounded linear logic, revisited. Zbl 1211.03090
Dal Lago, Ugo; Hofmann, Martin
2
2010
Verifying pointer and string analyses with region type systems. Zbl 1253.68092
Beringer, Lennart; Grabowski, Robert; Hofmann, Martin
2
2010
Verifying a local generic solver in Coq. Zbl 1306.68029
Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut
1
2010
Pure pointer programs with iteration. Zbl 1351.68101
Hofmann, Martin; Schöpp, Ulrich
1
2010
Bounded linear logic, revisited. Zbl 1211.03089
Dal Lago, Ugo; Hofmann, Martin
3
2009
Efficient type-checking for amortised heap-space analysis. Zbl 1257.68051
Hofmann, Martin; Rodriguez, Dulma
2
2009
Nominal renaming sets. Zbl 1182.03065
Gabbay, Murdoch J.; Hofmann, Martin
8
2008
Finite dimensional vector spaces are complete for traced symmetric monoidal categories. Zbl 1134.18003
Hasegawa, Masahito; Hofmann, Martin; Plotkin, Gordon
6
2008
A type system with usage aspects. Zbl 1142.68019
Aspinall, David; Hofmann, Martin; Konečný, Michal
3
2008
Certification using the Mobius base logic. Zbl 1209.68121
Beringer, Lennart; Hofmann, Martin; Pavlova, Mariela
2
2008
A program logic for resources. Zbl 1133.68010
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
8
2007
A proof system for the linear time \(\mu \)-calculus. Zbl 1163.03308
Dax, Christian; Hofmann, Martin; Lange, Martin
10
2006
Type-based amortised heap-space analysis. Zbl 1178.68143
Hofmann, Martin; Jost, Steffen
9
2006
Reading, writing and relations. Towards extensional semantics for effect analyses. Zbl 1168.68356
Benton, Nick; Kennedy, Andrew; Hofmann, Martin; Beringer, Lennart
6
2006
A bytecode logic for JML and types. Zbl 1168.68357
Beringer, Lennart; Hofmann, Martin
1
2006
Well-foundedness in realizability. Zbl 1112.03058
Hofmann, M.; van Oosten, J.; Streicher, T.
1
2006
Automatic certification of heap consumption. Zbl 1108.68374
Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha
8
2005
Quantitative models and implicit complexity. Zbl 1172.68477
Dal Lago, Ugo; Hofmann, Martin
6
2005
On the non-sequential nature of the interval-domain model of real-number computation. Zbl 1067.68070
Escardó, Martín; Hofmann, Martin; Streicher, Thomas
7
2004
Realizability models for BLL-like languages. Zbl 1047.03049
Hofmann, M.; Scott, P. J.
5
2004
An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036
Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut
4
2004
A program logic for resource verification. Zbl 1099.68584
Aspinall, 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.68180
Hofmann, Martin; Jost, Steffen
27
2003
Linear types and non-size-increasing polynomial time computation. Zbl 1054.68065
Hofmann, Martin
22
2003
The strength of non-size increasing computation. Zbl 1323.68213
Hofmann, Martin
7
2002
Completeness of continuation models for \(\lambda_\mu\)-calculus. Zbl 1096.03011
Hofmann, Martin; Streicher, Thomas
6
2002
A new “feasible” arithmetic. Zbl 1006.03035
Bellantoni, Stephen; Hofmann, Martin
5
2002
Safe recursion with higher types and BCK-algebra. Zbl 0959.68075
Hofmann, Martin
18
2000
A type system for bounded space and functional in-place update. Zbl 0971.68023
Hofmann, Martin
4
2000
A type system for bounded space and functional in-place update. (Extended abstract). Zbl 0964.68027
Hofmann, Martin
3
2000
Implementing a program logic of objects in a higher-order logic theorem prover. Zbl 0974.68185
Hofmann, Martin; Tang, Francis
2
2000
A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069
Coquand, Thierry; Hofmann, Martin
12
1999
Semantics of linear/modal lambda calculus. Zbl 0965.68011
Hofmann, Martin
2
1999
The groupoid interpretation of type theory. Zbl 0930.03089
Hofmann, Martin; Streicher, Thomas
38
1998
A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. Zbl 0908.03022
Hofmann, Martin
10
1998
Syntax and semantics of dependent types. Zbl 0919.68083
Hofmann, Martin
31
1997
Extensional constructs in intensional type theory. Zbl 1411.03001
Hofmann, Martin
7
1997
An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. Zbl 0931.03058
Hofmann, Martin
1
1997
On behavioural abstraction and behavioural satisfaction in higher-order logic. Zbl 0874.68196
Hofmann, Martin; Sannella, Donald
11
1996
Positive subtyping. Zbl 0853.68125
Hofmann, Martin; Pierce, Benjamin C.
4
1996
Conservativity of equality reflection over intensional type theory. Zbl 1434.03038
Hofmann, Martin
3
1996
On the interpretation of type theory in locally Cartesian closed categories. Zbl 1044.03544
Hofmann, Martin
20
1995
Sound and complete axiomatisations of call-by-value control operators. Zbl 0846.68066
Hofmann, Martin
8
1995
A simple model for quotient types. Zbl 1063.68602
Hofmann, Martin
2
1995
all top 5

Cited by 387 Authors

18 Hofmann, Martin
12 Dal Lago, Ugo
9 Baillot, Patrick
7 Palmgren, Erik
6 Albert, Elvira
6 Hennicker, Rolf
6 Lumsdaine, Peter LeFanu
5 Awodey, Steve
5 Beringer, Lennart
5 Coquand, Thierry
5 Hötzel Escardó, Martín
5 Pitts, Andrew M.
5 Zhang, Yu
4 Avigad, Jeremy
4 Bidoit, Michel
4 Birkedal, Lars
4 Gabbay, Murdoch James
4 Garner, Richard
4 Genaim, Samir
4 Peña, Ricardo
4 Warren, Michael Alton
3 Ariola, Zena M.
3 Aspinall, David
3 Berger, Ulrich
3 Dybjer, Peter
3 Florido, Mário
3 Herbelin, Hugo
3 Marcial-Romero, José Raymundo
3 Moerdijk, Ieke
3 Møgelberg, Rasmus Ejlers
3 Montenegro, Manuel
3 Nowak, David E.
3 Orton, Ian
3 Plotkin, Gordon D.
3 Puebla, Germán
3 Redmond, Brian F.
3 Schwichtenberg, Helmut
3 Segura, Clara
3 Streicher, Thomas
3 Studer, Thomas
3 Van den Berg, Benno
2 Abramsky, Samson
2 Ahrens, Benedikt
2 Altenkirch, Thorsten
2 Alves, Sandra
2 Arenas, Puri
2 Aubert, Clément
2 Avanzini, Martin
2 Barbanera, Franco
2 Bellantoni, Stephen J.
2 Benton, Nick
2 Brunel, Aloïs
2 Cantini, Andrea
2 Cockett, Robin
2 de’Liguoro, Ugo
2 Fernández, Maribel
2 Frohn, Florian
2 Ghani, Neil
2 Ghica, Dan R.
2 Giesl, Jürgen
2 Hähnle, Reiner
2 Harper, Robert
2 Hensel, Jera
2 Hernest, Mircea-Dan
2 Hofstra, Pieter J. W.
2 Hovland, Dag
2 Jagadeesan, Radha
2 Japaridze, Giorgi
2 Kapulkin, Krzysztof
2 Kock, Joachim
2 Lange, Martin
2 Mackie, Ian
2 Madeira, Alexandre
2 Martins, Manuel António
2 Matthes, Ralph
2 Moser, Georg
2 Moshier, M. Andrew
2 Moyen, Jean-Yves
2 Murawski, Andrzej S.
2 Nigam, Vivek
2 Niggl, Karl-Heinz
2 Power, John
2 Reddy, Uday S.
2 Saabas, Ando
2 Sabry, Amr
2 Sannella, Donald T.
2 Seidl, Helmut
2 Tabareau, Nicolas
2 Tarlecki, Andrzej
2 Terui, Kazushige
2 Uustalu, Tarmo
2 Vákár, Matthijs
2 Vogler, Ralf
2 Wirsing, Martin
2 Zanardini, Damiano
1 Abel, Andreas M.
1 Abou-Saleh, Faris
1 Accattoli, Beniamino
1 Aceto, Luca
1 Achten, Peter
...and 287 more Authors
all top 5

Cited in 40 Serials

44 Theoretical Computer Science
22 Annals of Pure and Applied Logic
21 Information and Computation
11 Journal of Automated Reasoning
11 Logical Methods in Computer Science
10 MSCS. Mathematical Structures in Computer Science
6 Journal of Functional Programming
5 The Journal of Symbolic Logic
5 The Journal of Logic and Algebraic Programming
4 Archive for Mathematical Logic
4 Journal of Applied Logic
4 Journal of Logical and Algebraic Methods in Programming
3 Formal Aspects of Computing
3 Indagationes Mathematicae. New Series
3 The Bulletin of Symbolic Logic
3 Theory of Computing Systems
3 Higher-Order and Symbolic Computation
3 ACM Transactions on Computational Logic
2 Journal of Pure and Applied Algebra
2 Studia Logica
2 Synthese
2 Science of Computer Programming
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 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 Formal Methods in System Design
1 Mathematical Logic Quarterly (MLQ)
1 Theory and Applications of Categories
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 Logica Universalis
1 Journal of Homotopy and Related Structures

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.