scientific article; zbMATH DE number 6680163

DOI10.4230/LIPICS.CSL.2013.653MaRDI QIDQ2958550zbMATH OpenFDO

Authors Qian Wang, Bruno Barras

Publication date 2 February 2017

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2013.653

zbMATH Keywords

calculus of constructionsconsistencyextensional type theoryintensional type theorymeta-theoryPresburger arithmeticset-theoretical modelstrong normalization

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Equational theories for inductive types
• scientific article; zbMATH DE number 6399373
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• scientific article; zbMATH DE number 139986
• Automated Deduction – CADE-20
• Extensional constructs in intensional type theory
• Intensional models for the theory of types
• Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality
• scientific article; zbMATH DE number 4027461
• Abstract deduction and inferential models for type theory

Cited in

(9)

• Functional verification of high performance adders in \textsc{Coq}
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Coq Modulo Theory
• Theory of types and decision procedures
• Coq without type casts: a complete proof of Coq Modulo Theory
• scientific article; zbMATH DE number 814613 (Why is no real title available?)
• Decidability in Intuitionistic Type Theory is Functionally Decidable
• Extensional and Intensional Semantic Universes
• scientific article; zbMATH DE number 6399373 (Why is no real title available?)

Describes a project that uses

Uses Software

• CoqMT
• CoqMTU
• Coq

This page was built for publication:

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