Elimination of Extensionality in Martin-Löf Type Theory. - Martin Hofmann 001 (TYPES, 1993)

On the Interpretation of Type Theory in Locally Cartesian Closed Categories. - Martin Hofmann 001 (CSL, 1994)

The Groupoid Model Refutes Uniqueness of Identity Proofs - Martin Hofmann 001; Thomas Streicher (LICS, 1994)

Categorical Reconstruction of a Reduction Free Normalization Proof. - Thorsten Altenkirch; Martin Hofmann 001; Thomas Streicher (Category Theory and Computer Science, 1995)

On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic. - Martin Hofmann 001; Donald Sannella (TAPSOFT, 1995)

A Simple Model for Quotient Types. - Martin Hofmann 001 (TLCA, 1995)

Conservativity of Equality Reflection over Intensional Type Theory. - Martin Hofmann 001 (TYPES, 1995)

A Unifying Type-Theoretic Framework for Objects. - Martin Hofmann 001; Benjamin C. Pierce (J. Funct. Program., 1995)

Sound and Complete Axiomatisations of Call-by-Value Control Operators. - Martin Hofmann 001 (Math. Struct. Comput. Sci., 1995)

Reduction-Free Normalisation for a Polymorphic System. - Thorsten Altenkirch; Martin Hofmann 001; Thomas Streicher (ISTCS, 1996)

Positive Subtyping. - Martin Hofmann 001; Benjamin C. Pierce (Inf. Comput., 1996)

On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic. - Martin Hofmann 001; Donald Sannella (Theor. Comput. Sci., 1996)

Extensional constructs in intensional type theory. - Martin Hofmann 001 (Springer, 1997)

A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion. - Martin Hofmann 001 (CSL, 1997)

Continuation Models are Universal for Lambda-Mu-Calculus. - Martin Hofmann 001; Thomas Streicher (LICS, 1997)

An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. - Martin Hofmann 001 (Bull. Symb. Log., 1997)

Inheritance of Proofs. - Martin Hofmann 001; Wolfgang Naraschewski; Martin Steffen; Terry Stroup (Theory Pract. Object Syst., 1998)

Semantical Analysis of Higher-Order Abstract Syntax. - Martin Hofmann 001 (LICS, 1999)

Semantics of Linear/Modal Lambda Calculus. - Martin Hofmann 001 (J. Funct. Program., 1999)

A new method for establishing conservativity of classical systems over their intuitionistic version. - Thierry Coquand; Martin Hofmann 001 (Math. Struct. Comput. Sci., 1999)

Preface. - Martin Hofmann 001; Giuseppe Rosolini; Dusko Pavlovic (CTCS, 1999)

A Type System for Bounded Space and Functional In-Place Update–Extended Abstract. - Martin Hofmann 001 (ESOP, 2000)

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. - Martin Hofmann 001; Francis Tang (TPHOLs, 2000)

Safe recursion with higher types and BCK-algebra. - Martin Hofmann 001 (Ann. Pure Appl. Log., 2000)

A Type System for Bounded Space and Functional In-Place Update. - Martin Hofmann 001 (Nord. J. Comput., 2000)

Programming languages capturing complexity classes. - Martin Hofmann 001 (SIGACT News, 2000)

Normalization by Evaluation for Typed Lambda Calculus with Coproducts. - Thorsten Altenkirch; Peter Dybjer; Martin Hofmann 001; Philip J. Scott (LICS, 2001)

The Strength of Non-size-increasing Computation (Introduction and Summary). - Martin Hofmann 001 (MFCS, 2001)

From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour. - Martin Hofmann 001 (TLCA, 2001)

Another Type System for In-Place Update. - David Aspinall 001; Martin Hofmann 001 (ESOP, 2002)

The strength of non-size increasing computation. - Martin Hofmann 001 (POPL, 2002)

Type Destructors. - Martin Hofmann 001; Benjamin C. Pierce (Inf. Comput., 2002)

Completeness of Continuation Models for lambda-mu-Calculus. - Martin Hofmann 001; Thomas Streicher (Inf. Comput., 2002)

A New "Feasible" Arithmetic. - Stephen J. Bellantoni; Martin Hofmann 001 (J. Symb. Log., 2002)

Certification of Memory Usage. - Martin Hofmann 001 (ICTCS, 2003)

Static prediction of heap space usage for first-order functional programs. - Martin Hofmann 001; Steffen Jost (POPL, 2003)

Linear types and non-size-increasing polynomial time computation. - Martin Hofmann 001 (Inf. Comput., 2003)

Preface. - Jirí Adámek; Martín Hötzel Escardó; Martin Hofmann 001 (Theor. Comput. Sci., 2003)

Mobile Resource Guarantees for Smart Devices. - David Aspinall 001; Stephen Gilmore; Martin Hofmann 001; Donald Sannella; Ian Stark (CASSIS, 2004)

04381 Abstracts Collection - Dependently Typed Programming. - Thorsten Altenkirch; Martin Hofmann 001; John Hughes 001 (Dependently Typed Programming, 2004)

What Do Program Logics and Type Systems Have in Common? - Martin Hofmann 001 (ICALP, 2004)

Automatic Certification of Heap Consumption. - Lennart Beringer; Martin Hofmann 001; Alberto Momigliano; Olha Shkaravska (LPAR, 2004)

A Program Logic for Resource Verification. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (TPHOLs, 2004)

On the non-sequential nature of the interval-domain model of real-number computation. - Martín Hötzel Escardó; Martin Hofmann 001; Thomas Streicher (Math. Struct. Comput. Sci., 2004)

An arithmetic for non-size-increasing polynomial-time computation. - Klaus Aehlig; Ulrich Berger 001; Martin Hofmann 001; Helmut Schwichtenberg (Theor. Comput. Sci., 2004)

Realizability models for BLL-like languages. - Martin Hofmann 001; Philip J. Scott (Theor. Comput. Sci., 2004)

Quantitative Models and Implicit Complexity. - Ugo Dal Lago; Martin Hofmann 001 (FSTTCS, 2005)

Proof-Theoretic Approach to Description-Logic. - Martin Hofmann 001 (LICS, 2005)

The Embounded project (project start paper). - Kevin Hammond; Roy Dyckhoff; Christian Ferdinand; Reinhold Heckmann; Martin Hofmann 001; Steffen Jost; Hans-Wolfgang Loidl; Greg Michaelson; Robert F. Pointon; Norman Scaife; Jocelyn Sérot; Andy Wallace (Trends in Functional Programming, 2005)

Mobile Resource Guarantees (project evaluation paper). - Donald Sannella; Martin Hofmann 001; David Aspinall 001; Stephen Gilmore; Ian Stark; Lennart Beringer; Hans-Wolfgang Loidl; Kenneth MacKenzie; Alberto Momigliano; Olha Shkaravska (Trends in Functional Programming, 2005)

Typed Lambda Calculi and Applications 2003, Selected Papers. - Martin Hofmann 001; Pawel Urzyczyn (Fundam. Informaticae, 2005)

Reading, Writing and Relations. - Nick Benton; Andrew Kennedy; Martin Hofmann 001; Lennart Beringer (APLAS, 2006)

Type-Based Amortised Heap-Space Analysis. - Martin Hofmann 001; Steffen Jost (ESOP, 2006)

A Proof System for the Linear Time µ-Calculus. - Christian Dax; Martin Hofmann 001; Martin Lange (FSTTCS, 2006)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

Towards Formally Verifiable WCET Analysis for a Functional Programming Language. - Kevin Hammond; Christian Ferdinand; Reinhold Heckmann; Roy Dyckhoff; Martin Hofmann 001; Steffen Jost; Hans-Wolfgang Loidl; Greg Michaelson; Robert F. Pointon; Norman Scaife; Jocelyn Sérot; Andy Wallace (WCET, 2006)

Well-foundedness in Realizability. - Martin Hofmann 001; Jaap van Oosten; Thomas Streicher (Arch. Math. Log., 2006)

Consistency of the theory of contexts. - Anna Bucalo; Furio Honsell; Marino Miculan; Ivan Scagnetto; Martin Hofmann 001 (J. Funct. Program., 2006)

Preface. - Martin Hofmann 001; Hans-Wolfgang Loidl (Theor. Comput. Sci., 2006)

Certification Using the Mobius Base Logic. - Lennart Beringer; Martin Hofmann 001; Mariela Pavlova (FMCO, 2007)

Relational semantics for effect-based program transformations with dynamic allocation. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2007)

Elimination of Ghost Variables in Program Logics. - Martin Hofmann 001; Mariela Pavlova (TGC, 2007)

A program logic for resources. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (Theor. Comput. Sci., 2007)

Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories. - Masahito Hasegawa; Martin Hofmann 001; Gordon D. Plotkin (Pillars of Computer Science, 2008)

08061 Executive Summary – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

08061 Abstracts Collection – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

Nominal Renaming Sets. - Murdoch James Gabbay; Martin Hofmann 001 (LPAR, 2008)

Secure information flow and program logics. - Lennart Beringer; Martin Hofmann 001 (Arch. Formal Proofs, 2008)

A Bytecode Logic for JML and Types. - Lennart Beringer; Martin Hofmann 001 (Arch. Formal Proofs, 2008)

Pointer Programs and Undirected Reachability. - Ulrich Schöpp; Martin Hofmann 001 (Electron. Colloquium Comput. Complex., 2008)

A type system with usage aspects. - David Aspinall 001; Martin Hofmann 001; Michal Konecný (J. Funct. Program., 2008)

Efficient Type-Checking for Amortised Heap-Space Analysis. - Martin Hofmann 001; Dulma Rodriguez (CSL, 2009)

Membership Checking in Greatest Fixpoints Revisited. - Martin Hofmann 001; Dulma Rodriguez (FICS, 2009)

"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. - Steffen Jost; Hans-Wolfgang Loidl; Kevin Hammond; Norman Scaife; Martin Hofmann 001 (FM, 2009)

Relational semantics for effect-based program transformations: higher-order store. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2009)

Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. - Jan Hoffmann 002; Martin Hofmann 001 (APLAS, 2010)

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

10351 Executive Summary - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

Amortized Resource Analysis with Polynomial Potential. - Jan Hoffmann 002; Martin Hofmann 001 (ESOP, 2010)

What Is a Pure Functional? - Martin Hofmann 001; Aleksandr Karbyshev; Helmut Seidl (ICALP (2), 2010)

Static determination of quantitative resource usage for higher-order programs. - Steffen Jost; Kevin Hammond; Hans-Wolfgang Loidl; Martin Hofmann 001 (POPL, 2010)

Type inference in intuitionistic linear logic. - Patrick Baillot; Martin Hofmann 001 (PPDP, 2010)

Verifying a Local Generic Solver in Coq. - Martin Hofmann 001; Aleksandr Karbyshev; Helmut Seidl (SAS, 2010)

Bounded Linear Logic, Revisited - Ugo Dal Lago; Martin Hofmann 001 (Log. Methods Comput. Sci., 2010)

A Semantic Proof of Polytime Soundness of Light Affine Logic. - Ugo Dal Lago; Martin Hofmann 001 (Theory Comput. Syst., 2010)

Pure pointer programs with iteration. - Martin Hofmann 001; Ulrich Schöpp (ACM Trans. Comput. Log., 2010)

Automatentheorie und Logik. - Martin Hofmann 001; Martin Lange (Springer, 2011)

Type-Based Enforcement of Secure Programming Guidelines - Code Injection Prevention at SAP. - Robert Grabowski; Martin Hofmann 001; Keqin Li 002 (Formal Aspects in Security and Trust, 2011)

Symmetric lenses. - Martin Hofmann 001; Benjamin C. Pierce; Daniel Wagner 001 (POPL, 2011)

Realizability models and implicit complexity. - Ugo Dal Lago; Martin Hofmann 001 (Theor. Comput. Sci., 2011)

Resource Aware ML. - Jan Hoffmann 002; Klaus Aehlig; Martin Hofmann 001 (CAV, 2012)

Linear Constraints over Infinite Trees. - Martin Hofmann 001; Dulma Rodriguez (LPAR, 2012)

Edit lenses. - Martin Hofmann 001; Benjamin C. Pierce; Daniel Wagner 001 (POPL, 2012)

Learn with SAT to Minimize Büchi Automata - Stephan Barth 001; Martin Hofmann 001 (GandALF, 2012)

Multivariate amortized resource analysis. - Jan Hoffmann 002; Klaus Aehlig; Martin Hofmann 001 (ACM Trans. Program. Lang. Syst., 2012)

Automatic Type Inference for Amortised Heap-Space Analysis. - Martin Hofmann 001; Dulma Rodriguez (ESOP, 2013)

On Monadic Parametricity of Second-Order Functionals. - Andrej Bauer; Martin Hofmann 001; Aleksandr Karbyshev (FoSSaCS, 2013)

Pure Pointer Programs and Tree Isomorphism. - Martin Hofmann 001; Ramyaa Ramyaa; Ulrich Schöpp (FoSSaCS, 2013)

Computing With a Fixed Number of Pointers (Invited Talk). - Martin Hofmann 001; Ramyaa (FSTTCS, 2013)

Verifying pointer and string analyses with region type systems. - Lennart Beringer; Robert Grabowski; Martin Hofmann 001 (Comput. Lang. Syst. Struct., 2013)

Power of Nondetreministic JAGs on Cayley graphs. - Martin Hofmann 001; Ramyaa Ramyaa (CoRR, 2013)

Edit languages for information trees. - Martin Hofmann 001; Benjamin C. Pierce; Daniel Wagner 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Abstract interpretation from Büchi automata. - Martin Hofmann 001; Wei Chen 023 (CSL-LICS, 2014)

Formal Semantics of Synchronous Transfer Architecture. - Gordon Cichon; Martin Hofmann 001 (Modellierung, 2014)

Abstract effects and proof-relevant logical relations. - Nick Benton; Martin Hofmann 001; Vivek Nigam (POPL, 2014)

Amortised Resource Analysis and Typed Polynomial Interpretations. - Martin Hofmann 001; Georg Moser (RTA-TLCA, 2014)

Büchi Types for Infinite Traces and Liveness. - Martin Hofmann 001; Wei Chen 023 (CoRR, 2014)

Amortised Resource Analysis and Typed Polynomial Interpretations (extended version). - Martin Hofmann 001; Georg Moser (CoRR, 2014)

Certification for mu-calculus with winning strategies. - Martin Hofmann 001; Harald Ruess (CoRR, 2014)

Revisiting the categorical interpretation of dependent type theory. - Pierre-Louis Curien; Richard Garner; Martin Hofmann 001 (Theor. Comput. Sci., 2014)

Logical Relations and Nondeterminism. - Martin Hofmann 001 (Software, Services, and Systems, 2015)

Automatic amortized analysis. - Martin Hofmann 001 (PPDP, 2015)

GuideForce: Type-Based Enforcement of Programming Guidelines. - Serdar Erbatur; Martin Hofmann 001 (SEFM Workshops, 2015)

Multivariate Amortised Resource Analysis for Term Rewrite Systems. - Martin Hofmann 001; Georg Moser (TLCA, 2015)

Modular Edit Lenses. - Martin Hofmann 001 (Bidirectional Transformations, 2016)

Counting Successes: Effects and Transformations for Non-deterministic Programs. - Nick Benton; Andrew Kennedy; Martin Hofmann 001; Vivek Nigam (A List of Successes That Can Change the World, 2016)

An Implementation of Deflate in Coq. - Christoph-Simon Senjak; Martin Hofmann 001 (FM, 2016)

Certification for μ-Calculus with Winning Strategies. - Martin Hofmann 001; Christian Neukirchen; Harald Rueß (SPIN, 2016)

From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112). - Andrej Bauer; Martin Hofmann 001; Matija Pretnar; Jeremy Yallop (Dagstuhl Reports, 2016)

Software-Verifikation. - Dirk Beyer 001; Rolf Hennicker; Martin Hofmann 001; Tobias Nipkow; Martin Wirsing (50 Jahre Universitäts-Informatik in München, 2017)

Enforcing Programming Guidelines with Region Types and Effects. - Serdar Erbatur; Martin Hofmann 001; Eugen Zalinescu (APLAS, 2017)

A cartesian-closed category for higher-order model checking. - Martin Hofmann 001; Jérémy Ledent (LICS, 2017)

Decidable linear list constraints. - Sabine Bauer 002; Martin Hofmann 001 (LPAR, 2017)

Decidable Inequalities over Infinite Trees. - Sabine Bauer 002; Steffen Jost; Martin Hofmann 001 (LPAR, 2018)

Linear Tree Constraints. - Sabine Bauer 002; Martin Hofmann 001 (CoRR, 2018)

Analysis of Logarithmic Amortised Complexity. - Martin Hofmann 001; Georg Moser (CoRR, 2018)

Proof-Relevant Logical Relations for Name Generation. - Nick Benton; Martin Hofmann 001; Vivek Nigam (Log. Methods Comput. Sci., 2018)

Effect-dependent transformations for concurrent programs. - Nick Benton; Martin Hofmann 001; Vivek Nigam (Sci. Comput. Program., 2018)

Foreword. - Martin Hofmann 001; David Aspinall 001; Brian Campbell 001; Ian Stark; Perdita Stevens (Theor. Comput. Sci., 2018)

A quantitative model for simply typed λ-calculus. - Martin Hofmann 001; Jérémy Ledent (Math. Struct. Comput. Sci., 2022)

Type-based analysis of logarithmic amortised complexity. - Martin Hofmann 001; Lorenz Leutgeb; David Obwaller; Georg Moser; Florian Zuleger (Math. Struct. Comput. Sci., 2022)