scientific article; zbMATH DE number 1301730

MaRDI QIDQ4246943zbMATH OpenFDO

Authors Jan Cederquist

Publication date 16 June 1999

zbMATH Keywords

abstract data typeclosed rational intervalcompactnesscontinuumformal spacesformal topologyHeine-Borel covering theoremimplementation in type theorypointfree formulationproof-checker Half

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Constructive and recursive analysis (03F60)

Recommendations

• Type theories from Barendregt's cube for theorem provers
• scientific article; zbMATH DE number 1302061
• Realizing Mahlo set theory in type theory
• A type theoretic interpretation of constructive domain theory
• scientific article; zbMATH DE number 1088206
• Proof theory of constructive systems: inductive types and univalence
• scientific article; zbMATH DE number 1302057
• A type-theoretic approach to induction with higher-order encodings
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• A modular construction of type theories

Cited in

(3)

• The Heine-Borel challenge problem. In honor of Woody Bledsoe
• Formal Zariski topology: Positivity and points
• Heirs of box types in polynomially bounded structures

Describes a project that uses

Uses Software

• ALF

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 Q4246943)