Logic of subtyping

DOI10.1016/J.TCS.2006.03.017MaRDI QIDQ2500487zbMATH OpenOpenAlexFDO

Authors 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

Curry-Howard isomorphismcut eliminationnonstandard logicproposition-as-typerecursive typessubtype

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1799515
• Judgmental subtyping systems with intersection types and modal types
• Theoretical Computer Science
• scientific article; zbMATH DE number 1114034
• A binary modal logic for the intersection types of lambda-calculus.

Cites work

• A binary modal logic for the intersection types of lambda-calculus.
• A lattice-theoretical fixpoint theorem and its applications
• A sequent calculus for subtyping polymorphic types
• An ideal model for recursive polymorphic types
• Coherence and transitivity of subtyping as entailment
• Combinatory logic. With two sections by William Craig.
• Efficient recursive subtyping
• Functionality in Combinatory Logic
• scientific article; zbMATH DE number 3862427 (Why is no real title available?)
• scientific article; zbMATH DE number 3928338 (Why is no real title available?)
• scientific article; zbMATH DE number 1183236 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3525100 (Why is no real title available?)
• scientific article; zbMATH DE number 512778 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1841844 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Inductive types and type constraints in the second-order lambda calculus
• Polymorphic type inference and containment
• Propositional lax logic
• The combinatory foundations of mathematical logic
• The semantics of entailment. II
• Type inference with recursive types: Syntax and semantics

Cited in

(13)

• Higher-order subtyping
• Logical equivalence for subtyping object and recursive types
• On modal logic of deductive closure
• Judgmental subtyping systems with intersection types and modal types
• Subtyping in logical form
• The relevance of semantic subtyping
• scientific article; zbMATH DE number 431770 (Why is no real title available?)
• scientific article; zbMATH DE number 512789 (Why is no real title available?)
• scientific article; zbMATH DE number 1114034 (Why is no real title available?)
• GADTs Meet Subtyping
• Theoretical Computer Science
• scientific article; zbMATH DE number 2242586 (Why is no real title available?)
• On modal logics of partial recursive functions

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Logic of subtyping

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2500487)