An implementation of LF with coercive subtyping and universes

DOI10.1023/A:1010648911114MaRDI QIDQ5951521zbMATH OpenOpenAlexFDO

Authors Paul Callaghan, Zhaohui Luo

Publication date 5 November 2003

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1010648911114

zbMATH Keywords

implementationlogical frameworktype theoryuniverses

Mathematics Subject Classification ID

Logic in computer science (03B70)

Review text

An implementation of a variant of Martin-Löf's logical framework with coercive subtyping, called LF, is presented. The paper begins with an outline of LF with its extensions of inductive types and coercions; then, motivations and the basic architecture of the implementation are given; finally, some examples are presented. In particular, special emphasis is put on the implementation of the the theory of a hierarchy of universes included in the object type theory UTT, which is outlined and implemented. The relationships between universes and inductive types, and between universes and coercive subtyping are studied and, as a conclusion, the authors claim that the combination of Tarski-style universes together with coercive subtyping provides an ideal formulation of universes that is both semantically clear and practical to use.

Recommendations

• Coercive subtyping for the calculus of constructions (extended abstract)
• scientific article; zbMATH DE number 1301735
• scientific article; zbMATH DE number 1086673
• scientific article; zbMATH DE number 1497873
• A coalgebraic semantics of subtyping
• A theory of typed coercions and its applications
• Formalization of a λ-calculus with explicit substitutions in Coq
• A computational view of implicit coercions in type theory
• Coercion completion and conservativity in coercive subtyping
• Coercive subtyping via mappings of reduction behaviour

Cited in

(11)

• Transitivity in coercive subtyping
• Natural language inference in Coq
• A pluralist approach to the formalisation of mathematics
• Coercions in a polymorphic type system
• Structural subtyping for inductive types with functorial equality rules
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• LF+ in Coq for "fast and loose" reasoning
• Coercion completion and conservativity in coercive subtyping
• Propositional forms of judgemental interpretations
• On subtyping in type theories with canonical objects
• A dependently-typed calculus of event telicity and culminativity

Describes a project that uses

Uses Software

• Plastic
• ALF

This page was built for publication: An implementation of LF with coercive subtyping and universes

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