Type theory should eat itself

DOI10.1016/J.ENTCS.2008.12.114MaRDI QIDQ2804938zbMATH OpenOpenAlexFDO

Authors James 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

Agdabig-step normalisationexplicit substitutionstype theorytyped 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)

Recommendations

• In the Search of a Naive Type Theory
• Do-it-yourself type theory
• scientific article; zbMATH DE number 4096759
• scientific article; zbMATH DE number 4096760
• scientific article; zbMATH DE number 733401
• scientific article; zbMATH DE number 2064184
• scientific article; zbMATH DE number 1302061
• scientific article; zbMATH DE number 604880
• Type theory with opposite types: a paraconsistent type theory
• Naïve Type Theory

Cites work

• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Big-step normalisation
• Dependently typed programming in Agda
• scientific article; zbMATH DE number 2185661 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 2006633 (Why is no real title available?)
• scientific article; zbMATH DE number 1863381 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Program testing and the meaning explanations of intuitionistic type theory
• Sets in Coq, Coq in Sets
• Towards formalizing categorical models of type theory in type theory
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

Cited in

(10)

• Shallow embedding of type theory is morally correct
• The \textsc{MetaCoq} project
• From realizability to induction via dependent intersection
• Extensible and efficient automation through reflective tactics
• Guarded recursion in Agda via sized types
• POPLMark reloaded: mechanizing proofs by logical relations
• Normalization by evaluation for modal dependent type theory
• Big step normalisation for type theory
• For Finitary Induction-Induction, Induction is Enough
• Touring the MetaCoq project

Describes a project that uses

Uses Software

• LEGO

This page was built for publication: Type theory should eat itself

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804938)