Dependently typed records in type theory

DOI10.1007/S001650200018MaRDI QIDQ699688zbMATH OpenOpenAlexFDO

Authors Robert Pollack

Publication date 25 September 2002

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s001650200018

zbMATH Keywords

dependent typessignaturemodulesharingpebbleinductive-recursivemanifest types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Data structures (68P05)

Recommendations

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

Cited in

(16)

• A record calculus with principal types
• Type classes for mathematics in type theory
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• scientific article; zbMATH DE number 2061705 (Why is no real title available?)
• Cayenne -- a language with dependent types
• Packaging Mathematical Structures
• Theories as types
• Cayenne -- a language with dependent types
• Pebble, a kernel language for modules and abstract data types
• Validating Mathematical Structures
• scientific article; zbMATH DE number 2182489 (Why is no real title available?)
• Variations on inductive-recursive definitions
• Working with Mathematical Structures in Type Theory
• scientific article; zbMATH DE number 2085166 (Why is no real title available?)
• Imperative LF meta-programming

Describes a project that uses

Uses Software

• LEGO

This page was built for publication: Dependently typed records in type theory

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