Admissibility of fixpoint induction over partial types

DOI10.1007/BFB0054265MaRDI QIDQ4249900zbMATH OpenFDO

Authors Karl Crary

Publication date 17 June 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://hdl.handle.net/1813/7328

zbMATH Keywords

admissible typesautomated theorem provingcompactnesscomputational approximation relationdependent productsmonotonicitypartial typespredicate-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: Admissibility of fixpoint induction over partial types

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