Coherence and transitivity of subtyping as entailment
From MaRDI portal
Publication:4507489
DOI10.1093/logcom/10.4.493zbMath0959.03042OpenAlexW2069624336MaRDI QIDQ4507489
Kathleen Milsted, Serguei V. Solov'ev
Publication date: 3 October 2000
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/75cf09f2ef487c5d9a6863e7788354f18bc9df7a
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05)
Related Items (5)
Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Coercions in a polymorphic type system ⋮ Transitivity in coercive subtyping ⋮ Logic of subtyping ⋮ Coercion completion and conservativity in coercive subtyping
This page was built for publication: Coherence and transitivity of subtyping as entailment