Martin Hofmann

According to our database1, Martin Hofmann authored at least 147 papers between 1993 and 2018.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
Foreword.
Theor. Comput. Sci., 2018

Effect-dependent transformations for concurrent programs.
Sci. Comput. Program., 2018

Proof-Relevant Logical Relations for Name Generation.
Logical Methods in Computer Science, 2018

Analysis of Logarithmic Amortised Complexity.
CoRR, 2018

Linear Tree Constraints.
CoRR, 2018

Enforcing Programming Guidelines with Region Types and Effects.
CoRR, 2018

Decidable Inequalities over Infinite Trees.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

2017
Proof-Relevant Logical Relations for Name Generation.
CoRR, 2017

Decidable linear list constraints.
Proceedings of the LPAR-21, 2017

A cartesian-closed category for higher-order model checking.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Enforcing Programming Guidelines with Region Types and Effects.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

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

An implementation of Deflate in Coq.
CoRR, 2016

Certification for μ-Calculus with Winning Strategies.
Proceedings of the Model Checking Software - 23rd International Symposium, 2016

Effect-dependent transformations for concurrent programs.
Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 2016

An Implementation of Deflate in Coq.
Proceedings of the FM 2016: Formal Methods, 2016

Counting Successes: Effects and Transformations for Non-deterministic Programs.
Proceedings of the A List of Successes That Can Change the World, 2016

Modular Edit Lenses.
Proceedings of the Bidirectional Transformations, 2016

2015
Effect-Dependent Transformations for Concurrent Programs.
CoRR, 2015

Multivariate Amortised Resource Analysis for Term Rewrite Systems.
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

GuideForce: Type-Based Enforcement of Programming Guidelines.
Proceedings of the Software Engineering and Formal Methods, 2015

Automatic amortized analysis.
Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015

Logical Relations and Nondeterminism.
Proceedings of the Software, 2015

2014
Revisiting the categorical interpretation of dependent type theory.
Theor. Comput. Sci., 2014

Certification for mu-calculus with winning strategies.
CoRR, 2014

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

Büchi Types for Infinite Traces and Liveness.
CoRR, 2014

Amortised Resource Analysis and Typed Polynomial Interpretations.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Abstract effects and proof-relevant logical relations.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Formal Semantics of Synchronous Transfer Architecture.
Proceedings of the Modellierung 2014, 19.-21. März 2014, Wien, Österreich, 2014

Abstract interpretation from Büchi automata.
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.
ECEASST, 2013

Power of Nondetreministic JAGs on Cayley graphs.
CoRR, 2013

Verifying pointer and string analyses with region type systems.
Computer Languages, Systems & Structures, 2013

Proof-Relevant Logical Relations for Name Generation.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Computing With a Fixed Number of Pointers (Invited Talk).
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

Pure Pointer Programs and Tree Isomorphism.
Proceedings of the Foundations of Software Science and Computation Structures, 2013

On Monadic Parametricity of Second-Order Functionals.
Proceedings of the Foundations of Software Science and Computation Structures, 2013

Automatic Type Inference for Amortised Heap-Space Analysis.
Proceedings of the Programming Languages and Systems, 2013

2012
Multivariate amortized resource analysis.
ACM Trans. Program. Lang. Syst., 2012

Abstract Effects and Proof-Relevant Logical Relations
CoRR, 2012

Learn with SAT to Minimize Büchi Automata
Proceedings of the Proceedings Third International Symposium on Games, 2012

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

Linear Constraints over Infinite Trees.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Resource Aware ML.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Realizability models and implicit complexity.
Theor. Comput. Sci., 2011

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

Multivariate amortized resource analysis.
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.
Proceedings of the Formal Aspects of Security and Trust - 8th International Workshop, 2011

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

2010
Pure pointer programs with iteration.
ACM Trans. Comput. Log., 2010

A Semantic Proof of Polytime Soundness of Light Affine Logic.
Theory Comput. Syst., 2010

Bounded Linear Logic, Revisited
Logical Methods in Computer Science, 2010

Verifying a Local Generic Solver in Coq.
Proceedings of the Static Analysis - 17th International Symposium, 2010

Type inference in intuitionistic linear logic.
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.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Verifying Pointer and String Analyses with Region Type Systems.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

What Is a Pure Functional?
Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Amortized Resource Analysis with Polynomial Potential.
Proceedings of the Programming Languages and Systems, 2010

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

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.
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.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Bounded Linear Logic, Revisited.
Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Relational semantics for effect-based program transformations: higher-order store.
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Pointer Programs and Undirected Reachability.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis.
Proceedings of the FM 2009: Formal Methods, 2009

Membership Checking in Greatest Fixpoints Revisited.
Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

Efficient Type-Checking for Amortised Heap-Space Analysis.
Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008
A type system with usage aspects.
J. Funct. Program., 2008

Pointer Programs and Undirected Reachability.
Electronic Colloquium on Computational Complexity (ECCC), 2008

A Bytecode Logic for JML and Types.
Archive of Formal Proofs, 2008

Secure information flow and program logics.
Archive of Formal Proofs, 2008

Nominal Renaming Sets.
Proceedings of the Logic for Programming, 2008

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

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

A Semantic Proof of Polytime Soundness of Light Affine Logic.
Proceedings of the Computer Science, 2008

Pure Pointer Programs with Iteration.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories.
Proceedings of the Pillars of Computer Science, 2008

2007
A program logic for resources.
Theor. Comput. Sci., 2007

Elimination of Ghost Variables in Program Logics.
Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Relational semantics for effect-based program transformations with dynamic allocation.
Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Certification Using the Mobius Base Logic.
Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Secure information flow and program logics.
Proceedings of the 20th IEEE Computer Security Foundations Symposium, 2007

2006
Preface.
Theor. Comput. Sci., 2006

Consistency of the theory of contexts.
J. Funct. Program., 2006

Well-foundedness in Realizability.
Arch. Math. Log., 2006

Towards Formally Verifiable WCET Analysis for a Functional Programming Language.
Proceedings of the 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2006

MOBIUS: Mobility, Ubiquity, Security.
Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

A Proof System for the Linear Time µ-Calculus.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Type-Based Amortised Heap-Space Analysis.
Proceedings of the Programming Languages and Systems, 2006

A Bytecode Logic for JML and Types.
Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

Reading, Writing and Relations.
Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005
Typed Lambda Calculi and Applications 2003, Selected Papers.
Fundam. Inform., 2005

Quantitative Models and Implicit Complexity
CoRR, 2005

Mobile Resource Guarantees (project evaluation paper).
Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

The Embounded project (project start paper).
Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

Proof-Theoretic Approach to Description-Logic.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Quantitative Models and Implicit Complexity.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004
Realizability models for BLL-like languages.
Theor. Comput. Sci., 2004

An arithmetic for non-size-increasing polynomial-time computation.
Theor. Comput. Sci., 2004

On the non-sequential nature of the interval-domain model of real-number computation.
Mathematical Structures in Computer Science, 2004

A Program Logic for Resource Verification.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Automatic Certification of Heap Consumption.
Proceedings of the Logic for Programming, 2004

What Do Program Logics and Type Systems Have in Common?
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

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

Mobile Resource Guarantees for Smart Devices.
Proceedings of the Construction and Analysis of Safe, 2004

2003
Preface.
Theor. Comput. Sci., 2003

Linear types and non-size-increasing polynomial time computation.
Inf. Comput., 2003

Static prediction of heap space usage for first-order functional programs.
Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Certification of Memory Usage.
Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2002
A New "Feasible" Arithmetic.
J. Symb. Log., 2002

Completeness of Continuation Models for lambda-mu-Calculus.
Inf. Comput., 2002

Type Destructors.
Inf. Comput., 2002

The strength of non-size increasing computation.
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.
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.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

The Strength of Non-size-increasing Computation (Introduction and Summary).
Proceedings of the Mathematical Foundations of Computer Science 2001, 2001

Normalization by Evaluation for Typed Lambda Calculus with Coproducts.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000
Programming languages capturing complexity classes.
SIGACT News, 2000

A Type System for Bounded Space and Functional In-Place Update.
Nord. J. Comput., 2000

Safe recursion with higher types and BCK-algebra.
Ann. Pure Appl. Logic, 2000

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.
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.
Proceedings of the Programming Languages and Systems, 2000

1999
Preface.
Electr. Notes Theor. Comput. Sci., 1999

A new method for establishing conservativity of classical systems over their intuitionistic version.
Mathematical Structures in Computer Science, 1999

Semantics of Linear/Modal Lambda Calculus.
J. Funct. Program., 1999

Linear Types and Non-Size-Increasing Polynomial Time Computation.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Semantical Analysis of Higher-Order Abstract Syntax.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998
Inheritance of Proofs.
TAPOS, 1998

1997
An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras.
Bulletin of Symbolic Logic, 1997

Continuation Models are Universal for Lambda-Mu-Calculus.
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.
Proceedings of the Computer Science Logic, 11th International Workshop, 1997

Extensional constructs in intensional type theory.
CPHC/BCS distinguished dissertations, Springer, ISBN: 978-3-540-76121-1, 1997

1996
On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic.
Theor. Comput. Sci., 1996

Positive Subtyping.
Inf. Comput., 1996

Reduction-Free Normalisation for a Polymorphic System.
Proceedings of the Proceedings, 1996

1995
Sound and Complete Axiomatisations of Call-by-Value Control Operators.
Mathematical Structures in Computer Science, 1995

A Unifying Type-Theoretic Framework for Objects.
J. Funct. Program., 1995

Conservativity of Equality Reflection over Intensional Type Theory.
Proceedings of the Types for Proofs and Programs, 1995

A Simple Model for Quotient Types.
Proceedings of the Typed Lambda Calculi and Applications, 1995

On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Positive Subtyping.
Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

Categorical Reconstruction of a Reduction Free Normalization Proof.
Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1994
A Unifying Type-Theoretic Framework for Objects.
Proceedings of the STACS 94, 1994

The Groupoid Model Refutes Uniqueness of Identity Proofs
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.
Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993
Elimination of Extensionality in Martin-Löf Type Theory.
Proceedings of the Types for Proofs and Programs, 1993


  Loading...