Coherence and transitivity of subtyping as entailment

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

zbMATH Keywords

polymorphismsecond-order logiccut-eliminationcoercive subtypingGentzen sequent calculus

Mathematics Subject Classification ID

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