Coercive subtyping
From MaRDI portal
Publication:4238487
DOI10.1093/logcom/9.1.105zbMath0920.03062OpenAlexW4243054153MaRDI QIDQ4238487
Publication date: 30 March 1999
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/082432bdb9cc0abb8c554c0ba2cae862ccc48fa9
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (18)
Hints in Unification ⋮ Working with Mathematical Structures in Type Theory ⋮ Propositional forms of judgemental interpretations ⋮ A constructive algebraic hierarchy in Coq. ⋮ Coercions in a polymorphic type system ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ User interaction with the Matita proof assistant ⋮ Adjectival and adverbial modification: the view from modern type theories ⋮ A User Interface for a Mathematical System that Allows Ambiguous Formulae ⋮ 2-Dimensional Directed Type Theory ⋮ Natural language inference in Coq ⋮ Transitivity in coercive subtyping ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Coercion completion and conservativity in coercive subtyping ⋮ Subtyping dependent types ⋮ The Matita Interactive Theorem Prover ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Taming the Merge Operator
This page was built for publication: Coercive subtyping
