Dependently typed records in type theory

DOI10.1007/s001650200018zbMath1001.68013OpenAlexW2002193175MaRDI QIDQ699688

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

signaturepebblemoduledependent typessharinginductive-recursivemanifest types

Mathematics Subject Classification ID

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

Related Items

Validating Mathematical Structures ⋮ Packaging Mathematical Structures ⋮ Working with Mathematical Structures in Type Theory ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Type classes for mathematics in type theory ⋮ Variations on inductive-recursive definitions ⋮ Imperative LF Meta-Programming

Uses Software

• LEGO