Coherence of subsumption, minimum typing and type-checking in F ≤
From MaRDI portal
Publication:4005456
DOI10.1017/S0960129500001134zbMath0765.03008MaRDI QIDQ4005456
Pierre-Louis Curien, Giorgio Ghelli
Publication date: 27 September 1992
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
completenesssoundnesstype checkingtypingsemi-decision procedurecoherence of subsumptionnormalizing rewriting techniquesecond-order lambda calculus with bounded quantificationsemantic coherence
Related Items (24)
An operational semantics for TOOPLE: A statically-typed object-oriented programming language ⋮ A meta-language for typed object-oriented languages ⋮ Higher-order subtyping and its decidability ⋮ Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping ⋮ Size-based termination of higher-order rewriting ⋮ Termination of system \(F\)-bounded: A complete proof ⋮ Bounded existentials and minimal typing ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Higher-order subtyping ⋮ Typed operational semantics for higher-order subtyping. ⋮ Divergence of \(F_{\leq}\) type checking ⋮ R n - and G n -logics ⋮ Subtyping recursion and parametric polymorphism in kernel Fun ⋮ Subtyping dependent types ⋮ Coherence of subsumption for monadic types ⋮ Game Semantics for Bounded Polymorphism ⋮ Dependent type system with subtyping I: Type level transitivity elimination ⋮ Unnamed Item ⋮ Basic theory of \(F\)-bounded quantification. ⋮ Comparing object encodings. ⋮ A sequent calculus for subtyping polymorphic types ⋮ Type destructors ⋮ A paradigmatic object-oriented programming language: Design, static typing and semantics ⋮ Simple type-theoretic foundations for object-oriented programming
Cites Work
This page was built for publication: Coherence of subsumption, minimum typing and type-checking in F ≤
