A sequent calculus for subtyping polymorphic types

DOI10.1006/inco.2000.2941zbMath1007.03011OpenAlexW2081748224WikidataQ61634973 ScholiaQ61634973MaRDI QIDQ1854408

Jerzy Tiuryn

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/f9466642821565f24379a9c9a964ede7709d0b1a

zbMATH Keywords

coherencecut eliminationnatural deductionsubtypingpolymorphic typessubject reductionGentzen-style sequent calculusdecidability of type reconstruction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Logic of subtyping

Cites Work

• Unnamed Item
• Unnamed Item
• On the unity of logic
• Functorial polymorphism
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A modest model of records, inheritance, and bounded quantification
• Polymorphic type inference and containment
• Constructivism in mathematics. An introduction. Volume I
• An extension of system \(F\) with subtyping
• Equational axiomatization of bicoercibility for polymorphic types
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Embedding first order predicate logic in fragments of intuitionistic logic
• On 2nd order intuitionistic propositional calculus with full comprehension

This page was built for publication: A sequent calculus for subtyping polymorphic types