Constructor subtyping in the calculus of inductive constructions

DOI10.1007/3-540-46432-8_2MaRDI QIDQ4508290zbMATH OpenFDO

Authors Gilles Barthe, Femke van Raamsdonk

Publication date 3 October 2000

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

Full work available at URL https://doi.org/10.1007/3-540-46432-8_2

zbMATH Keywords

Calculus of Inductive Constructionsconstructor subtypingproof-development systemssemantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Subtyping calculus of construction. (Extended abstract)
• A calculus of constructions with explicit subtyping
• Inductively defined types in the Calculus of Constructions
• scientific article; zbMATH DE number 1156716
• scientific article; zbMATH DE number 2061701
• scientific article; zbMATH DE number 2182487
• scientific article; zbMATH DE number 7526056
• Coercive subtyping for the calculus of constructions (extended abstract)
• Constructing inductive-inductive types in cubical type theory
• Semantics of typed lambda-calculus with constructors

Cited in

(15)

• Dependent type system with subtyping I: Type level transitivity elimination
• Transitivity in coercive subtyping
• Principles and pragmatics of subtyping in PVS
• Implementation techniques for inductive types in Plastic
• The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping
• scientific article; zbMATH DE number 431766 (Why is no real title available?)
• Structural recursive definitions in type theory
• Subtyping calculus of construction. (Extended abstract)
• Relating Church-style and Curry-style subtyping
• Typed operational semantics for dependent record types
• scientific article; zbMATH DE number 7526056 (Why is no real title available?)
• A calculus of constructions with explicit subtyping
• Theorem Proving in Higher Order Logics
• Higher-order subtyping and its decidability
• Program self-reference in constructive Scott subdomains

Describes a project that uses

Uses Software

• Coq
• LEGO

This page was built for publication: Constructor subtyping in the calculus of inductive constructions

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