Martin Hofmann

160 papers A* 20A 7B 20C 5Misc 1Journal 55Unranked 43

Year	Rank	Type	Title / Venue / Authors
2022	J	`jnl`	A quantitative model for simply typed λ-calculus. Math. Struct. Comput. Sci. Martin Hofmann, Jérémy Ledent
2022	J	`jnl`	Type-based analysis of logarithmic amortised complexity. Math. Struct. Comput. Sci. Martin Hofmann, Lorenz Leutgeb, David Obwaller, Georg Moser, Florian Zuleger
2021	J	`jnl`	Type-Based Analysis of Logarithmic Amortised Complexity. CoRR Martin Hofmann, Lorenz Leutgeb, Georg Moser, David Obwaller, Florian Zuleger
2018	J	`jnl`	Analysis of Logarithmic Amortised Complexity. CoRR Martin Hofmann, Georg Moser
2018	B	`conf`	Decidable Inequalities over Infinite Trees. LPAR Sabine Bauer, Steffen Jost, Martin Hofmann
2018	J	`jnl`	Effect-dependent transformations for concurrent programs. Sci. Comput. Program. Nick Benton, Martin Hofmann, Vivek Nigam
2018	J	`jnl`	Enforcing Programming Guidelines with Region Types and Effects. CoRR Serdar Erbatur, Martin Hofmann, Eugen Zalinescu
2018	J	`jnl`	Foreword. Theor. Comput. Sci. Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens
2018	J	`jnl`	Linear Tree Constraints. CoRR Sabine Bauer, Martin Hofmann
2018	J	`jnl`	Proof-Relevant Logical Relations for Name Generation. Log. Methods Comput. Sci. Nick Benton, Martin Hofmann, Vivek Nigam
2017	A*	`conf`	A cartesian-closed category for higher-order model checking. LICS Martin Hofmann, Jérémy Ledent
2017	B	`conf`	Decidable linear list constraints. LPAR Sabine Bauer, Martin Hofmann
2017	B	`conf`	Enforcing Programming Guidelines with Region Types and Effects. APLAS Serdar Erbatur, Martin Hofmann, Eugen Zalinescu
2017	J	`jnl`	Proof-Relevant Logical Relations for Name Generation. CoRR Nick Benton, Martin Hofmann, Vivek Nigam
2017	—	`ch.`	Software-Verifikation. 50 Jahre Universitäts-Informatik in München Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing
2016	B	`conf`	An Implementation of Deflate in Coq. FM Christoph-Simon Senjak, Martin Hofmann
2016	J	`jnl`	An implementation of Deflate in Coq. CoRR Christoph-Simon Senjak, Martin Hofmann
2016	—	`conf`	Certification for μ-Calculus with Winning Strategies. SPIN Martin Hofmann, Christian Neukirchen, Harald Rueß
2016	—	`conf`	Counting Successes: Effects and Transformations for Non-deterministic Programs. A List of Successes That Can Change the World Nick Benton, Andrew Kennedy, Martin Hofmann, Vivek Nigam
2016	C	`conf`	Effect-dependent transformations for concurrent programs. PPDP Nick Benton, Martin Hofmann, Vivek Nigam
2016	J	`jnl`	From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112). Dagstuhl Reports Andrej Bauer, Martin Hofmann, Matija Pretnar, Jeremy Yallop
2016	—	`conf`	Modular Edit Lenses. Bidirectional Transformations Martin Hofmann
2015	C	`conf`	Automatic amortized analysis. PPDP Martin Hofmann
2015	J	`jnl`	Effect-Dependent Transformations for Concurrent Programs. CoRR Nick Benton, Martin Hofmann, Vivek Nigam
2015	—	`conf`	GuideForce: Type-Based Enforcement of Programming Guidelines. SEFM Workshops Serdar Erbatur, Martin Hofmann
2015	—	`conf`	Logical Relations and Nondeterminism. Software, Services, and Systems Martin Hofmann
2015	—	`conf`	Multivariate Amortised Resource Analysis for Term Rewrite Systems. TLCA Martin Hofmann, Georg Moser
2014	A*	`conf`	Abstract effects and proof-relevant logical relations. POPL Nick Benton, Martin Hofmann, Vivek Nigam
2014	—	`conf`	Abstract interpretation from Büchi automata. CSL-LICS Martin Hofmann, Wei Chen
2014	J	`jnl`	Amortised Resource Analysis and Typed Polynomial Interpretations (extended version). CoRR Martin Hofmann, Georg Moser
2014	—	`conf`	Amortised Resource Analysis and Typed Polynomial Interpretations. RTA-TLCA Martin Hofmann, Georg Moser
2014	J	`jnl`	Büchi Types for Infinite Traces and Liveness. CoRR Martin Hofmann, Wei Chen
2014	J	`jnl`	Certification for mu-calculus with winning strategies. CoRR Martin Hofmann, Harald Ruess
2014	—	`conf`	Formal Semantics of Synchronous Transfer Architecture. Modellierung Gordon Cichon, Martin Hofmann
2014	J	`jnl`	Revisiting the categorical interpretation of dependent type theory. Theor. Comput. Sci. Pierre-Louis Curien, Richard Garner, Martin Hofmann
2013	A	`conf`	Automatic Type Inference for Amortised Heap-Space Analysis. ESOP Martin Hofmann, Dulma Rodriguez
2013	—	`conf`	Computing With a Fixed Number of Pointers (Invited Talk). FSTTCS Martin Hofmann, Ramyaa
2013	J	`jnl`	Edit languages for information trees. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Martin Hofmann, Benjamin C. Pierce, Daniel Wagner
2013	B	`conf`	On Monadic Parametricity of Second-Order Functionals. FoSSaCS Andrej Bauer, Martin Hofmann, Aleksandr Karbyshev
2013	J	`jnl`	Power of Nondetreministic JAGs on Cayley graphs. CoRR Martin Hofmann, Ramyaa Ramyaa
2013	—	`conf`	Proof-Relevant Logical Relations for Name Generation. TLCA Nick Benton, Martin Hofmann, Vivek Nigam
2013	B	`conf`	Pure Pointer Programs and Tree Isomorphism. FoSSaCS Martin Hofmann, Ramyaa Ramyaa, Ulrich Schöpp
2013	J	`jnl`	Verifying pointer and string analyses with region type systems. Comput. Lang. Syst. Struct. Lennart Beringer, Robert Grabowski, Martin Hofmann
2012	J	`jnl`	Abstract Effects and Proof-Relevant Logical Relations CoRR Nick Benton, Martin Hofmann, Vivek Nigam
2012	A*	`conf`	Edit lenses. POPL Martin Hofmann, Benjamin C. Pierce, Daniel Wagner
2012	—	`conf`	Learn with SAT to Minimize Büchi Automata GandALF Stephan Barth, Martin Hofmann
2012	B	`conf`	Linear Constraints over Infinite Trees. LPAR Martin Hofmann, Dulma Rodriguez
2012	J	`jnl`	Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2012	A*	`conf`	Resource Aware ML. CAV Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2011	—	`book`	Automatentheorie und Logik. Martin Hofmann, Martin Lange
2011	B	`ed.`	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 FoSSaCS Martin Hofmann
2011	A*	`conf`	Multivariate amortized resource analysis. POPL Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2011	J	`jnl`	Realizability models and implicit complexity. Theor. Comput. Sci. Ugo Dal Lago, Martin Hofmann
2011	A*	`conf`	Symmetric lenses. POPL Martin Hofmann, Benjamin C. Pierce, Daniel Wagner
2011	—	`conf`	Type-Based Enforcement of Secure Programming Guidelines - Code Injection Prevention at SAP. Formal Aspects in Security and Trust Robert Grabowski, Martin Hofmann, Keqin Li
2010	—	`conf`	10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010	—	`conf`	10351 Executive Summary - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010	J	`jnl`	A Semantic Proof of Polytime Soundness of Light Affine Logic. Theory Comput. Syst. Ugo Dal Lago, Martin Hofmann
2010	B	`conf`	Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. APLAS Jan Hoffmann, Martin Hofmann
2010	A	`conf`	Amortized Resource Analysis with Polynomial Potential. ESOP Jan Hoffmann, Martin Hofmann
2010	J	`jnl`	Bounded Linear Logic, Revisited Log. Methods Comput. Sci. Ugo Dal Lago, Martin Hofmann
2010	—	`ed.`	Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010 Modelling, Controlling and Reasoning About State Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010	J	`jnl`	Pure pointer programs with iteration. ACM Trans. Comput. Log. Martin Hofmann, Ulrich Schöpp
2010	A*	`conf`	Static determination of quantitative resource usage for higher-order programs. POPL Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann
2010	—	`ed.`	Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers TGC Martin Wirsing, Martin Hofmann, Axel Rauschmayer
2010	C	`conf`	Type inference in intuitionistic linear logic. PPDP Patrick Baillot, Martin Hofmann
2010	—	`conf`	Verifying Pointer and String Analyses with Region Type Systems. LPAR (Dakar) Lennart Beringer, Robert Grabowski, Martin Hofmann
2010	B	`conf`	Verifying a Local Generic Solver in Coq. SAS Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl
2010	—	`conf`	What Is a Pure Functional? ICALP (2) Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl
2009	B	`conf`	"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. FM Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann
2009	—	`conf`	Bounded Linear Logic, Revisited. TLCA Ugo Dal Lago, Martin Hofmann
2009	B	`conf`	Efficient Type-Checking for Amortised Heap-Space Analysis. CSL Martin Hofmann, Dulma Rodriguez
2009	—	`conf`	Membership Checking in Greatest Fixpoints Revisited. FICS Martin Hofmann, Dulma Rodriguez
2009	A*	`conf`	Pointer Programs and Undirected Reachability. LICS Martin Hofmann, Ulrich Schöpp
2009	C	`conf`	Relational semantics for effect-based program transformations: higher-order store. PPDP Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
2008	—	`conf`	08061 Abstracts Collection -- Types, Logics and Semantics for State. Types, Logics and Semantics for State Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
2008	—	`conf`	08061 Executive Summary -- Types, Logics and Semantics for State. Types, Logics and Semantics for State Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
2008	J	`jnl`	A Bytecode Logic for JML and Types. Arch. Formal Proofs Lennart Beringer, Martin Hofmann
2008	Misc	`conf`	A Semantic Proof of Polytime Soundness of Light Affine Logic. CSR Ugo Dal Lago, Martin Hofmann
2008	J	`jnl`	A type system with usage aspects. J. Funct. Program. David Aspinall, Martin Hofmann, Michal Konecný
2008	—	`conf`	Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories. Pillars of Computer Science Masahito Hasegawa, Martin Hofmann, Gordon D. Plotkin
2008	B	`conf`	Nominal Renaming Sets. LPAR Murdoch James Gabbay, Martin Hofmann
2008	J	`jnl`	Pointer Programs and Undirected Reachability. Electron. Colloquium Comput. Complex. Ulrich Schöpp, Martin Hofmann
2008	B	`conf`	Pure Pointer Programs with Iteration. CSL Martin Hofmann, Ulrich Schöpp
2008	J	`jnl`	Secure information flow and program logics. Arch. Formal Proofs Lennart Beringer, Martin Hofmann
2008	—	`ed.`	Types, Logics and Semantics for State, 03.02. - 08.02.2008 Types, Logics and Semantics for State Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
2007	J	`jnl`	A program logic for resources. Theor. Comput. Sci. David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
2007	—	`conf`	Certification Using the Mobius Base Logic. FMCO Lennart Beringer, Martin Hofmann, Mariela Pavlova
2007	—	`conf`	Elimination of Ghost Variables in Program Logics. TGC Martin Hofmann, Mariela Pavlova
2007	A*	`ed.`	Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007 POPL Martin Hofmann, Matthias Felleisen
2007	C	`conf`	Relational semantics for effect-based program transformations with dynamic allocation. PPDP Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
2007	A	`conf`	Secure information flow and program logics. CSF Lennart Beringer, Martin Hofmann
2006	B	`conf`	A Bytecode Logic for JML and Types. APLAS Lennart Beringer, Martin Hofmann
2006	—	`conf`	A Proof System for the Linear Time µ-Calculus. FSTTCS Christian Dax, Martin Hofmann, Martin Lange
2006	J	`jnl`	Consistency of the theory of contexts. J. Funct. Program. Anna Bucalo, Furio Honsell, Marino Miculan, Ivan Scagnetto, Martin Hofmann
2006	—	`conf`	MOBIUS: Mobility, Ubiquity, Security. TGC 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
2006	J	`jnl`	Preface. Theor. Comput. Sci. Martin Hofmann, Hans-Wolfgang Loidl
2006	B	`conf`	Reading, Writing and Relations. APLAS Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer
2006	—	`conf`	Towards Formally Verifiable WCET Analysis for a Functional Programming Language. WCET 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
2006	A	`conf`	Type-Based Amortised Heap-Space Analysis. ESOP Martin Hofmann, Steffen Jost
2006	J	`jnl`	Well-foundedness in Realizability. Arch. Math. Log. Martin Hofmann, Jaap van Oosten, Thomas Streicher
2005	—	`conf`	Mobile Resource Guarantees (project evaluation paper). Trends in Functional Programming Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska
2005	A*	`conf`	Proof-Theoretic Approach to Description-Logic. LICS Martin Hofmann
2005	J	`jnl`	Quantitative Models and Implicit Complexity CoRR Ugo Dal Lago, Martin Hofmann
2005	—	`conf`	Quantitative Models and Implicit Complexity. FSTTCS Ugo Dal Lago, Martin Hofmann
2005	—	`conf`	The Embounded project (project start paper). Trends in Functional Programming 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
2005	J	`jnl`	Typed Lambda Calculi and Applications 2003, Selected Papers. Fundam. Informaticae Martin Hofmann, Pawel Urzyczyn
2004	—	`conf`	04381 Abstracts Collection - Dependently Typed Programming. Dependently Typed Programming Thorsten Altenkirch, Martin Hofmann, John Hughes
2004	—	`conf`	A Program Logic for Resource Verification. TPHOLs David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
2004	J	`jnl`	An arithmetic for non-size-increasing polynomial-time computation. Theor. Comput. Sci. Klaus Aehlig, Ulrich Berger, Martin Hofmann, Helmut Schwichtenberg
2004	B	`conf`	Automatic Certification of Heap Consumption. LPAR Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
2004	—	`ed.`	Dependently Typed Programming, 12.09. - 17.09.2004 Dependently Typed Programming Thorsten Altenkirch, Martin Hofmann, John Hughes
2004	—	`conf`	Mobile Resource Guarantees for Smart Devices. CASSIS David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark
2004	J	`jnl`	On the non-sequential nature of the interval-domain model of real-number computation. Math. Struct. Comput. Sci. Martín Hötzel Escardó, Martin Hofmann, Thomas Streicher
2004	J	`jnl`	Realizability models for BLL-like languages. Theor. Comput. Sci. Martin Hofmann, Philip J. Scott
2004	A*	`conf`	What Do Program Logics and Type Systems Have in Common? ICALP Martin Hofmann
2003	—	`conf`	Certification of Memory Usage. ICTCS Martin Hofmann
2003	J	`jnl`	Linear types and non-size-increasing polynomial time computation. Inf. Comput. Martin Hofmann
2003	J	`jnl`	Preface. Theor. Comput. Sci. Jirí Adámek, Martín Hötzel Escardó, Martin Hofmann
2003	A*	`conf`	Static prediction of heap space usage for first-order functional programs. POPL Martin Hofmann, Steffen Jost
2003	—	`ed.`	Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings. TLCA Martin Hofmann
2002	J	`jnl`	A New "Feasible" Arithmetic. J. Symb. Log. Stephen J. Bellantoni, Martin Hofmann
2002	A	`conf`	Another Type System for In-Place Update. ESOP David Aspinall, Martin Hofmann
2002	J	`jnl`	Completeness of Continuation Models for lambda-mu-Calculus. Inf. Comput. Martin Hofmann, Thomas Streicher
2002	A*	`conf`	The strength of non-size increasing computation. POPL Martin Hofmann
2002	J	`jnl`	Type Destructors. Inf. Comput. Martin Hofmann, Benjamin C. Pierce
2001	—	`conf`	From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour. TLCA Martin Hofmann
2001	A*	`conf`	Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
2001	B	`conf`	The Strength of Non-size-increasing Computation (Introduction and Summary). MFCS Martin Hofmann
2000	A	`conf`	A Type System for Bounded Space and Functional In-Place Update--Extended Abstract. ESOP Martin Hofmann
2000	J	`jnl`	A Type System for Bounded Space and Functional In-Place Update. Nord. J. Comput. Martin Hofmann
2000	—	`conf`	Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. TPHOLs Martin Hofmann, Francis Tang
2000	J	`jnl`	Programming languages capturing complexity classes. SIGACT News Martin Hofmann
2000	J	`jnl`	Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Log. Martin Hofmann
1999	J	`jnl`	A new method for establishing conservativity of classical systems over their intuitionistic version. Math. Struct. Comput. Sci. Thierry Coquand, Martin Hofmann
1999	—	`ed.`	Conference on Category Theory and Computer Science, CTCS 1999, Edinburgh, UK, December 10-12, 1999 CTCS Martin Hofmann, Giuseppe Rosolini, Dusko Pavlovic
1999	A*	`conf`	Linear Types and Non-Size-Increasing Polynomial Time Computation. LICS Martin Hofmann
1999	—	`conf`	Preface. CTCS Martin Hofmann, Giuseppe Rosolini, Dusko Pavlovic
1999	A*	`conf`	Semantical Analysis of Higher-Order Abstract Syntax. LICS Martin Hofmann
1999	J	`jnl`	Semantics of Linear/Modal Lambda Calculus. J. Funct. Program. Martin Hofmann
1998	J	`jnl`	Inheritance of Proofs. Theory Pract. Object Syst. Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, Terry Stroup
1997	B	`conf`	A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion. CSL Martin Hofmann
1997	J	`jnl`	An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. Bull. Symb. Log. Martin Hofmann
1997	A*	`conf`	Continuation Models are Universal for Lambda-Mu-Calculus. LICS Martin Hofmann, Thomas Streicher
1997	—	`book`	Extensional constructs in intensional type theory. Martin Hofmann
1996	J	`jnl`	On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic. Theor. Comput. Sci. Martin Hofmann, Donald Sannella
1996	J	`jnl`	Positive Subtyping. Inf. Comput. Martin Hofmann, Benjamin C. Pierce
1996	—	`conf`	Reduction-Free Normalisation for a Polymorphic System. ISTCS Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1996	A*	`conf`	Reduction-Free Normalisation for a Polymorphic System. LICS Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1995	—	`conf`	A Simple Model for Quotient Types. TLCA Martin Hofmann
1995	J	`jnl`	A Unifying Type-Theoretic Framework for Objects. J. Funct. Program. Martin Hofmann, Benjamin C. Pierce
1995	—	`conf`	Categorical Reconstruction of a Reduction Free Normalization Proof. Category Theory and Computer Science Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1995	—	`conf`	Conservativity of Equality Reflection over Intensional Type Theory. TYPES Martin Hofmann
1995	—	`conf`	On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic. TAPSOFT Martin Hofmann, Donald Sannella
1995	A*	`conf`	Positive Subtyping. POPL Martin Hofmann, Benjamin C. Pierce
1995	J	`jnl`	Sound and Complete Axiomatisations of Call-by-Value Control Operators. Math. Struct. Comput. Sci. Martin Hofmann
1994	A	`conf`	A Unifying Type-Theoretic Framework for Objects. STACS Martin Hofmann, Benjamin C. Pierce
1994	B	`conf`	On the Interpretation of Type Theory in Locally Cartesian Closed Categories. CSL Martin Hofmann
1994	A*	`conf`	The Groupoid Model Refutes Uniqueness of Identity Proofs LICS Martin Hofmann, Thomas Streicher
1993	—	`conf`	Elimination of Extensionality in Martin-Löf Type Theory. TYPES Martin Hofmann