An implementation of LF with coercive subtyping and universes

DOI10.1023/A:1010648911114zbMath1023.03020OpenAlexW1813213602MaRDI QIDQ5951521

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

implementationtype theorylogical frameworkuniverses

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (8)

Propositional forms of judgemental interpretations ⋮ Coercions in a polymorphic type system ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Natural language inference in Coq ⋮ Transitivity in coercive subtyping ⋮ Coercion completion and conservativity in coercive subtyping ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ A pluralist approach to the formalisation of mathematics

Uses Software

• Plastic
• ALF

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