Type Theory Should Eat Itself

DOI10.1016/j.entcs.2008.12.114zbMath1337.68057OpenAlexW2147289514MaRDI QIDQ2804938

James T. E. Chapman

Publication date: 6 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.114

zbMATH Keywords

type theoryexplicit substitutionsAgdabig-step normalisationtyped syntax

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

From realizability to induction via dependent intersection ⋮ Normalization by evaluation for modal dependent type theory ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ The \textsc{MetaCoq} project ⋮ Unnamed Item ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Unnamed Item ⋮ Extensible and Efficient Automation Through Reflective Tactics

Uses Software

• LEGO

Cites Work

• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Big-step normalisation
• Dependently Typed Programming in Agda
• Program Testing and the Meaning Explanations of Intuitionistic Type Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item