scientific article; zbMATH DE number 1303347

MaRDI QIDQ4249900zbMATH OpenFDO

Authors Karl Crary

Publication date 17 June 1999

zbMATH Keywords

compactnessmonotonicityautomated theorem provingdependent productspartial typesadmissible typescomputational approximation relationpredicate-admissibility

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Partiality, state and dependent types
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Partial inductive definitions as type-systems for \(\lambda\)-terms
• scientific article; zbMATH DE number 1863381
• Remarks on Martin-Löf's partial type theory

Cited in

(3)

• \(\Sigma\)-predicates of finite types over an admissible set
• Partiality, state and dependent types
• HYBRID PARTIAL-TOTAL TYPE THEORY

Describes a project that uses

Uses Software

• Nuprl
• 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 Q4249900)