Logic of subtyping

DOI10.1016/j.tcs.2006.03.017zbMath1094.03020OpenAlexW1968739019MaRDI QIDQ2500487

Pavel Naumov

Publication date: 16 August 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.03.017

zbMATH Keywords

cut eliminationCurry-Howard isomorphismrecursive typesnonstandard logicproposition-as-typesubtype

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

On modal logic of deductive closure, On modal logics of partial recursive functions

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type inference with recursive types: Syntax and semantics
• Combinatory logic. With two sections by William Craig.
• Polymorphic type inference and containment
• The semantics of entailment. II
• Propositional lax logic
• A binary modal logic for the intersection types of lambda-calculus.
• A sequent calculus for subtyping polymorphic types
• Inductive types and type constraints in the second-order lambda calculus
• A lattice-theoretical fixpoint theorem and its applications
• An ideal model for recursive polymorphic types
• Coherence and transitivity of subtyping as entailment
• Functionality in Combinatory Logic
• Efficient recursive subtyping
• HYBRID PARTIAL-TOTAL TYPE THEORY
• The combinatory foundations of mathematical logic