Type theory should eat itself
DOI10.1016/J.ENTCS.2008.12.114zbMATH Open1337.68057OpenAlexW2147289514MaRDI QIDQ2804938FDOQ2804938
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
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
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)
Cites Work
- Dependently typed programming in Agda
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Sets in Coq, Coq in Sets
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Towards formalizing categorical models of type theory in type theory
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Big-step normalisation
Cited In (9)
- The \textsc{MetaCoq} project
- Extensible and Efficient Automation Through Reflective Tactics
- From realizability to induction via dependent intersection
- POPLMark reloaded: Mechanizing proofs by logical relations
- Title not available (Why is that?)
- Normalization by evaluation for modal dependent type theory
- Shallow embedding of type theory is morally correct
- Title not available (Why is that?)
- For Finitary Induction-Induction, Induction is Enough
Uses Software
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)
