Soundness and principal contexts for a shallow polymorphic type system based on classical logic

DOI10.1093/JIGPAL/JZQ013zbMATH Open1259.03046OpenAlexW2108441139MaRDI QIDQ2889577FDOQ2889577

Authors: Alexander J. Summers 

Publication date: 8 June 2012

Published in: Logic Journal of the IGPL (Search for Journal in Brave)

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

Recommendations

• Programming Languages and Systems
• scientific article; zbMATH DE number 1222431
• Completeness and soundness results for \(\mathcal X\) with intersection and union types
• A sequent calculus for subtyping polymorphic types
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)

zbMATH Keywords

Curry-Howard correspondencecut eliminationclassical logicprincipal typesgeneric unificationshallow polymorphism

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (3)

• Programming Languages and Systems
• Monadic translation of classical sequent calculus
• Shallow embedding of type theory is morally correct

Uses Software

• ML

This page was built for publication: Soundness and principal contexts for a shallow polymorphic type system based on classical logic

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