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

DOI10.1093/JIGPAL/JZQ013MaRDI QIDQ2889577zbMATH OpenOpenAlexFDO

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

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)

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}\)

Cited in

(3)

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

Describes a project that uses

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)