Manifest Fields and Module Mechanisms in Intensional Type Theory

DOI10.1007/978-3-642-02444-3_15zbMath1246.68092OpenAlexW1555972076MaRDI QIDQ3638256

Zhaohui Luo

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02444-3_15

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Uses Software

• Coq
• ML
• Nuprl
• Plastic
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependently typed records in type theory
• Innovations in computational type theory using Nuprl
• Pebble, a kernel language for modules and abstract data types
• Singleton, union, and intersection types for program extraction
• Transitivity in coercive subtyping
• A higher-order calculus and theory abstraction
• Working with Mathematical Structures in Type Theory
• Coercions in a polymorphic type system
• Structural subtyping for inductive types with functorial equality rules
• Coercive subtyping
• Simple type-theoretic foundations for object-oriented programming
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping

This page was built for publication: Manifest Fields and Module Mechanisms in Intensional Type Theory