scientific article; zbMATH DE number 1302055

MaRDI QIDQ4247299zbMATH OpenFDO

Authors Gustavo Betarte, Álvaro Tasistro

Publication date 16 June 1999

zbMATH Keywords

subtypingabstract data typesconstructive type theoryalgebraic systemssetoidsdependent record typesMartin-Löf's set theoryrecord type inclusiontype formation

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• scientific article; zbMATH DE number 814798
• scientific article; zbMATH DE number 3853066
• Dependently typed records in type theory
• scientific article; zbMATH DE number 1187955
• A calculus with recursive types, record concatenation and subtyping
• scientific article; zbMATH DE number 1342292
• Remarks on Martin-Löf's partial type theory
• Martin-Löf's type theory as an open-ended framework
• Subtyping and intersection types revisited
• Extensional constructs in intensional type theory

Cited in

(12)

• A record calculus with principal types
• scientific article; zbMATH DE number 1187955 (Why is no real title available?)
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Subtyping dependent types
• Packaging Mathematical Structures
• Theories as types
• Innovations in computational type theory using Nuprl
• scientific article; zbMATH DE number 2182489 (Why is no real title available?)
• Working with Mathematical Structures in Type Theory
• scientific article; zbMATH DE number 1088047 (Why is no real title available?)
• Martin-Löf's type theory as an open-ended framework
• Implicit coercions in type systems

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