Martin Hofmann

According to our database, Martin Hofmann authored at least 131 papers between 1993 and 2022.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2022

Type-based analysis of logarithmic amortised complexity.

Martin Hofmann, Lorenz Leutgeb, David Obwaller, Georg Moser, Florian Zuleger

Math. Struct. Comput. Sci., June, 2022

A quantitative model for simply typed λ-calculus.

Martin Hofmann, Jérémy Ledent

Math. Struct. Comput. Sci., June, 2022

2018

Foreword.

Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens

Theor. Comput. Sci., 2018

Effect-dependent transformations for concurrent programs.

Nick Benton, Martin Hofmann, Vivek Nigam

Sci. Comput. Program., 2018

Proof-Relevant Logical Relations for Name Generation.

Nick Benton, Martin Hofmann, Vivek Nigam

Log. Methods Comput. Sci., 2018

Analysis of Logarithmic Amortised Complexity.

Martin Hofmann, Georg Moser

CoRR, 2018

Linear Tree Constraints.

Sabine Bauer, Martin Hofmann

CoRR, 2018

Decidable Inequalities over Infinite Trees.

Sabine Bauer, Steffen Jost, Martin Hofmann

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

2017

Decidable linear list constraints.

Sabine Bauer, Martin Hofmann

Proceedings of the LPAR-21, 2017

A cartesian-closed category for higher-order model checking.

Martin Hofmann, Jérémy Ledent

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Enforcing Programming Guidelines with Region Types and Effects.

Serdar Erbatur, Martin Hofmann, Eugen Zalinescu

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

Software-Verifikation.

Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing

Proceedings of the 50 Jahre Universitäts-Informatik in München, 2017

2016

From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112).

Andrej Bauer, Martin Hofmann, Matija Pretnar, Jeremy Yallop

Dagstuhl Reports, 2016

Certification for μ-Calculus with Winning Strategies.

Martin Hofmann, Christian Neukirchen, Harald Rueß

Proceedings of the Model Checking Software - 23rd International Symposium, 2016

An Implementation of Deflate in Coq.

Christoph-Simon Senjak, Martin Hofmann

Proceedings of the FM 2016: Formal Methods, 2016

Counting Successes: Effects and Transformations for Non-deterministic Programs.

Nick Benton, Andrew Kennedy, Martin Hofmann, Vivek Nigam

Proceedings of the A List of Successes That Can Change the World, 2016

Modular Edit Lenses.

Martin Hofmann

Proceedings of the Bidirectional Transformations, 2016

2015

Multivariate Amortised Resource Analysis for Term Rewrite Systems.

Martin Hofmann, Georg Moser

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

GuideForce: Type-Based Enforcement of Programming Guidelines.

Serdar Erbatur, Martin Hofmann

Proceedings of the Software Engineering and Formal Methods, 2015

Automatic amortized analysis.

Martin Hofmann

Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015

Logical Relations and Nondeterminism.

Martin Hofmann

Proceedings of the Software, 2015

2014

Revisiting the categorical interpretation of dependent type theory.

Pierre-Louis Curien, Richard Garner, Martin Hofmann

Theor. Comput. Sci., 2014

Certification for mu-calculus with winning strategies.

Martin Hofmann, Harald Ruess

CoRR, 2014

Amortised Resource Analysis and Typed Polynomial Interpretations (extended version).

Martin Hofmann, Georg Moser

CoRR, 2014

Büchi Types for Infinite Traces and Liveness.

Martin Hofmann, Wei Chen

CoRR, 2014

Amortised Resource Analysis and Typed Polynomial Interpretations.

Martin Hofmann, Georg Moser

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Abstract effects and proof-relevant logical relations.

Nick Benton, Martin Hofmann, Vivek Nigam

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Formal Semantics of Synchronous Transfer Architecture.

Gordon Cichon, Martin Hofmann

Proceedings of the Modellierung 2014, 19.-21. März 2014, Wien, Österreich, 2014

Abstract interpretation from Büchi automata.

Martin Hofmann, Wei Chen

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

Edit languages for information trees.

Martin Hofmann, Benjamin C. Pierce, Daniel Wagner

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013

Power of Nondetreministic JAGs on Cayley graphs.

Martin Hofmann, Ramyaa Ramyaa

CoRR, 2013

Verifying pointer and string analyses with region type systems.

Lennart Beringer, Robert Grabowski, Martin Hofmann

Comput. Lang. Syst. Struct., 2013

Computing With a Fixed Number of Pointers (Invited Talk).

Martin Hofmann, Ramyaa

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

Pure Pointer Programs and Tree Isomorphism.

Martin Hofmann, Ramyaa Ramyaa, Ulrich Schöpp

Proceedings of the Foundations of Software Science and Computation Structures, 2013

On Monadic Parametricity of Second-Order Functionals.

Andrej Bauer, Martin Hofmann, Aleksandr Karbyshev

Proceedings of the Foundations of Software Science and Computation Structures, 2013

Automatic Type Inference for Amortised Heap-Space Analysis.

Martin Hofmann, Dulma Rodriguez

Proceedings of the Programming Languages and Systems, 2013

2012

Multivariate amortized resource analysis.

Jan Hoffmann, Klaus Aehlig, Martin Hofmann

ACM Trans. Program. Lang. Syst., 2012

Learn with SAT to Minimize Büchi Automata

Stephan Barth, Martin Hofmann

Proceedings of the Proceedings Third International Symposium on Games, 2012

Edit lenses.

Martin Hofmann, Benjamin C. Pierce, Daniel Wagner

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Linear Constraints over Infinite Trees.

Martin Hofmann, Dulma Rodriguez

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Resource Aware ML.

Jan Hoffmann, Klaus Aehlig, Martin Hofmann

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Realizability models and implicit complexity.

Ugo Dal Lago, Martin Hofmann

Theor. Comput. Sci., 2011

Symmetric lenses.

Martin Hofmann, Benjamin C. Pierce, Daniel Wagner

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Type-Based Enforcement of Secure Programming Guidelines - Code Injection Prevention at SAP.

Robert Grabowski, Martin Hofmann, Keqin Li

Proceedings of the Formal Aspects of Security and Trust - 8th International Workshop, 2011

Automatentheorie und Logik.

Martin Hofmann, Martin Lange

eXamen.press, Springer, ISBN: 978-3-642-18089-7, 2011

2010

Pure pointer programs with iteration.

Martin Hofmann, Ulrich Schöpp

ACM Trans. Comput. Log., 2010

A Semantic Proof of Polytime Soundness of Light Affine Logic.

Ugo Dal Lago, Martin Hofmann

Theory Comput. Syst., 2010

Bounded Linear Logic, Revisited

Ugo Dal Lago, Martin Hofmann

Log. Methods Comput. Sci., 2010

Verifying a Local Generic Solver in Coq.

Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl

Proceedings of the Static Analysis - 17th International Symposium, 2010

Type inference in intuitionistic linear logic.

Patrick Baillot, Martin Hofmann

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

Static determination of quantitative resource usage for higher-order programs.

Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

What Is a Pure Functional?

Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl

Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Amortized Resource Analysis with Polynomial Potential.

Jan Hoffmann, Martin Hofmann

Proceedings of the Programming Languages and Systems, 2010

10351 Executive Summary - Modelling, Controlling and Reasoning About State.

Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.

Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics.

Jan Hoffmann, Martin Hofmann

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Relational semantics for effect-based program transformations: higher-order store.

Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis.

Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann

Proceedings of the FM 2009: Formal Methods, 2009

Membership Checking in Greatest Fixpoints Revisited.

Martin Hofmann, Dulma Rodriguez

Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

Efficient Type-Checking for Amortised Heap-Space Analysis.

Martin Hofmann, Dulma Rodriguez

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008

A type system with usage aspects.

David Aspinall, Martin Hofmann, Michal Konecný

J. Funct. Program., 2008

Pointer Programs and Undirected Reachability.

Ulrich Schöpp, Martin Hofmann

Electron. Colloquium Comput. Complex., 2008

A Bytecode Logic for JML and Types.

Lennart Beringer, Martin Hofmann

Arch. Formal Proofs, 2008

Secure information flow and program logics.

Lennart Beringer, Martin Hofmann

Arch. Formal Proofs, 2008

Nominal Renaming Sets.

Murdoch James Gabbay, Martin Hofmann

Proceedings of the Logic for Programming, 2008

08061 Abstracts Collection -- Types, Logics and Semantics for State.

Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

08061 Executive Summary -- Types, Logics and Semantics for State.

Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories.

Masahito Hasegawa, Martin Hofmann, Gordon D. Plotkin

Proceedings of the Pillars of Computer Science, 2008

2007

A program logic for resources.

David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano

Theor. Comput. Sci., 2007

Elimination of Ghost Variables in Program Logics.

Martin Hofmann, Mariela Pavlova

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Relational semantics for effect-based program transformations with dynamic allocation.

Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Certification Using the Mobius Base Logic.

Lennart Beringer, Martin Hofmann, Mariela Pavlova

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006

Preface.

Martin Hofmann, Hans-Wolfgang Loidl

Theor. Comput. Sci., 2006

Consistency of the theory of contexts.

Anna Bucalo, Furio Honsell, Marino Miculan, Ivan Scagnetto, Martin Hofmann

J. Funct. Program., 2006

Well-foundedness in Realizability.

Martin Hofmann, Jaap van Oosten, Thomas Streicher

Arch. Math. Log., 2006

Towards Formally Verifiable WCET Analysis for a Functional Programming Language.

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert F. Pointon, Norman Scaife, Jocelyn Sérot, Andy Wallace

Proceedings of the 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2006

MOBIUS: Mobility, Ubiquity, Security.

Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

A Proof System for the Linear Time µ-Calculus.

Christian Dax, Martin Hofmann, Martin Lange

Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Type-Based Amortised Heap-Space Analysis.

Martin Hofmann, Steffen Jost

Proceedings of the Programming Languages and Systems, 2006

Reading, Writing and Relations.

Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer

Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005

Typed Lambda Calculi and Applications 2003, Selected Papers.

Martin Hofmann, Pawel Urzyczyn

Fundam. Informaticae, 2005

Mobile Resource Guarantees (project evaluation paper).

Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

The Embounded project (project start paper).

Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert F. Pointon, Norman Scaife, Jocelyn Sérot, Andy Wallace

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

Proof-Theoretic Approach to Description-Logic.

Martin Hofmann

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Quantitative Models and Implicit Complexity.

Ugo Dal Lago, Martin Hofmann

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004

Realizability models for BLL-like languages.

Martin Hofmann, Philip J. Scott

Theor. Comput. Sci., 2004

An arithmetic for non-size-increasing polynomial-time computation.

Klaus Aehlig, Ulrich Berger, Martin Hofmann, Helmut Schwichtenberg

Theor. Comput. Sci., 2004

On the non-sequential nature of the interval-domain model of real-number computation.

Martín Hötzel Escardó, Martin Hofmann, Thomas Streicher

Math. Struct. Comput. Sci., 2004

A Program Logic for Resource Verification.

David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Automatic Certification of Heap Consumption.

Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska

Proceedings of the Logic for Programming, 2004

What Do Program Logics and Type Systems Have in Common?

Martin Hofmann

Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

04381 Abstracts Collection - Dependently Typed Programming.

Thorsten Altenkirch, Martin Hofmann, John Hughes

Proceedings of the Dependently Typed Programming, 12.09. - 17.09.2004, 2004

Mobile Resource Guarantees for Smart Devices.

David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark

Proceedings of the Construction and Analysis of Safe, 2004

2003

Preface.

Jirí Adámek, Martín Hötzel Escardó, Martin Hofmann

Theor. Comput. Sci., 2003

Linear types and non-size-increasing polynomial time computation.

Martin Hofmann

Inf. Comput., 2003

Static prediction of heap space usage for first-order functional programs.

Martin Hofmann, Steffen Jost

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Certification of Memory Usage.

Martin Hofmann

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2002

A New "Feasible" Arithmetic.

Stephen J. Bellantoni, Martin Hofmann

J. Symb. Log., 2002

Completeness of Continuation Models for lambda-mu-Calculus.

Martin Hofmann, Thomas Streicher

Inf. Comput., 2002

Type Destructors.

Martin Hofmann, Benjamin C. Pierce

Inf. Comput., 2002

The strength of non-size increasing computation.

Martin Hofmann

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Another Type System for In-Place Update.

David Aspinall, Martin Hofmann

Proceedings of the Programming Languages and Systems, 2002

2001

From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour.

Martin Hofmann

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

The Strength of Non-size-increasing Computation (Introduction and Summary).

Martin Hofmann

Proceedings of the Mathematical Foundations of Computer Science 2001, 2001

Normalization by Evaluation for Typed Lambda Calculus with Coproducts.

Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

Programming languages capturing complexity classes.

Martin Hofmann

SIGACT News, 2000

A Type System for Bounded Space and Functional In-Place Update.

Martin Hofmann

Nord. J. Comput., 2000

Safe recursion with higher types and BCK-algebra.

Martin Hofmann

Ann. Pure Appl. Log., 2000

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.

Martin Hofmann, Francis Tang

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

A Type System for Bounded Space and Functional In-Place Update--Extended Abstract.

Martin Hofmann

Proceedings of the Programming Languages and Systems, 2000

1999

Preface.

Martin Hofmann, Giuseppe Rosolini, Dusko Pavlovic

Proceedings of the Conference on Category Theory and Computer Science, 1999

A new method for establishing conservativity of classical systems over their intuitionistic version.

Thierry Coquand, Martin Hofmann

Math. Struct. Comput. Sci., 1999

Semantics of Linear/Modal Lambda Calculus.

Martin Hofmann

J. Funct. Program., 1999

Semantical Analysis of Higher-Order Abstract Syntax.

Martin Hofmann

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998

Inheritance of Proofs.

Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, Terry Stroup

Theory Pract. Object Syst., 1998

1997

An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras.

Martin Hofmann

Bull. Symb. Log., 1997

Continuation Models are Universal for Lambda-Mu-Calculus.

Martin Hofmann, Thomas Streicher

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion.

Martin Hofmann

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

Extensional constructs in intensional type theory.

Martin Hofmann

CPHC/BCS distinguished dissertations, Springer, ISBN: 978-3-540-76121-1, 1997

1996

On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic.

Martin Hofmann, Donald Sannella

Theor. Comput. Sci., 1996

Positive Subtyping.

Martin Hofmann, Benjamin C. Pierce

Inf. Comput., 1996

Reduction-Free Normalisation for a Polymorphic System.

Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

Proceedings of the Fourth Israel Symposium on Theory of Computing and Systems, 1996

1995

Sound and Complete Axiomatisations of Call-by-Value Control Operators.

Martin Hofmann

Math. Struct. Comput. Sci., 1995

A Unifying Type-Theoretic Framework for Objects.

Martin Hofmann, Benjamin C. Pierce

J. Funct. Program., 1995

Conservativity of Equality Reflection over Intensional Type Theory.

Martin Hofmann

Proceedings of the Types for Proofs and Programs, 1995

A Simple Model for Quotient Types.

Martin Hofmann

Proceedings of the Typed Lambda Calculi and Applications, 1995

On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic.

Martin Hofmann, Donald Sannella

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Categorical Reconstruction of a Reduction Free Normalization Proof.

Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1994

The Groupoid Model Refutes Uniqueness of Identity Proofs

Martin Hofmann, Thomas Streicher

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

On the Interpretation of Type Theory in Locally Cartesian Closed Categories.

Martin Hofmann

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993

Elimination of Extensionality in Martin-Löf Type Theory.

Martin Hofmann

Proceedings of the Types for Proofs and Programs, 1993