ETA-RULES IN MARTIN-LÖF TYPE THEORY

DOI10.1017/bsl.2019.21zbMath1486.03028OpenAlexW2963738827MaRDI QIDQ5240810

Ansten Mørch Klev

Publication date: 29 October 2019

Published in: The Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/61ab60707ef269e96e05124d376cf5bc6dca4902

zbMATH Keywords

type theoryjustification of logical lawsdefinitional identity

Mathematics Subject Classification ID

Structure of proofs (03F07) Type theory (03B38)

Related Items (1)

Spiritus asper versus lambda: on the nature of functional abstraction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Recursive number theory. A development of recursive arithmetic in a logic-free equation calculus
• Combinatory logic. With two sections by William Craig.
• Do-it-yourself type theory
• On the strength of dependent products in the type theory of Martin-Löf
• Inductive families
• Conditionally reversible computations and weak universality in category theory
• Proof-theoretic harmony: towards an intensional account
• A judgmental reconstruction of modal logic
• λ-definable functionals andβη conversion
• A natural extension of natural deduction
• A framework for defining logics
• A coherence theorem for Martin-Löf's type theory
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Extensional Constructs in Intensional Type Theory
• Identity of Proofs Based on Normalization and Generality
• Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections
• Intensional interpretations of functionals of finite type I
• The Mechanical Evaluation of Expressions

This page was built for publication: ETA-RULES IN MARTIN-LÖF TYPE THEORY