scientific article; zbMATH DE number 1187955

MaRDI QIDQ3840769zbMATH OpenFDO

Authors Gustavo Betarte

Publication date 11 August 1998

zbMATH Keywords

Martin-Löf's type theorymechanical verificationproof checker

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Abstract data types; algebraic specification (68Q65)

Recommendations

• Type checking dependent (record) types and subtyping
• scientific article; zbMATH DE number 1302055
• scientific article; zbMATH DE number 2061705
• scientific article; zbMATH DE number 2182489

Cited in

(13)

• Order-sorted inductive types
• Theories as types
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• scientific article; zbMATH DE number 1301741 (Why is no real title available?)
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• scientific article; zbMATH DE number 2061705 (Why is no real title available?)
• Type checking dependent (record) types and subtyping
• scientific article; zbMATH DE number 2182489 (Why is no real title available?)
• scientific article; zbMATH DE number 2085166 (Why is no real title available?)
• scientific article; zbMATH DE number 1420790 (Why is no real title available?)
• A record calculus with principal types
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Dependently typed records in type theory

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