Logic of subtyping

DOI10.1016/J.TCS.2006.03.017zbMATH Open1094.03020OpenAlexW1968739019MaRDI QIDQ2500487FDOQ2500487

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

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.

zbMATH Keywords

Curry-Howard isomorphismcut eliminationrecursive typesnonstandard logicproposition-as-typesubtype

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (10)

• On modal logic of deductive closure
• The relevance of semantic subtyping
• Theoretical Computer Science
• Title not available (Why is that?)
• Logical equivalence for subtyping object and recursive types
• Higher-order subtyping
• GADTs Meet Subtyping
• Subtyping in logical form
• Title not available (Why is that?)
• On modal logics of partial recursive functions

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)