What does it take to certify a conversion checker?
From MaRDI portal
Cites work
- A partial type checking algorithm for Type:Type
- A syntactic approach to type soundness
- An adequacy theorem for dependent type theory
- An algorithm for type-checking dependent types
- Candle: a verified implementation of HOL light
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
- For the metatheory of type theory, internal sconing is enough
- scientific article; zbMATH DE number 5173450 (Why is no real title available?)
- scientific article; zbMATH DE number 7699441 (Why is no real title available?)
- Normalization by evaluation for modal dependent type theory
- Parallel reductions in \(\lambda\)-calculus
- Proof-assistants using dependent type systems
- Pure type system conversion is always typable
- Pure type systems with judgemental equality
- Turing-Completeness Totally Free
This page was built for publication: What does it take to certify a conversion checker?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7296822)
