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

Agdatype theoryexplicit substitutionsbig-step normalisationtyped syntax

Mathematics Subject Classification ID

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

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

• 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?)
• 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
• 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

(9)

• POPLMark reloaded: mechanizing proofs by logical relations
• Extensible and efficient automation through reflective tactics
• Normalization by evaluation for modal dependent type theory
• Shallow embedding of type theory is morally correct
• From realizability to induction via dependent intersection
• For Finitary Induction-Induction, Induction is Enough
• scientific article; zbMATH DE number 7559298 (Why is no real title available?)
• Big step normalisation for type theory
• The \textsc{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)