Dependently typed records in type theory

DOI10.1007/S001650200018zbMATH Open1001.68013OpenAlexW2002193175MaRDI QIDQ699688FDOQ699688

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

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

zbMATH Keywords

dependent typessignaturemodulesharingpebbleinductive-recursivemanifest types

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cayenne -- a language with dependent types
• Packaging Mathematical Structures
• Theories as types
• Cayenne -- a language with dependent types
• Validating Mathematical Structures
• Pebble, a kernel language for modules and abstract data types
• Title not available (Why is that?)
• Variations on inductive-recursive definitions
• Working with Mathematical Structures in Type Theory
• Title not available (Why is that?)
• Imperative LF meta-programming

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)