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

DOI10.1093/JIGPAL/JZQ013zbMath1259.03046OpenAlexW2108441139MaRDI QIDQ2889577

Alexander J. Summers

Publication date: 8 June 2012

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

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

zbMATH Keywords

cut eliminationclassical logicCurry-Howard correspondenceprincipal typesgeneric unificationshallow polymorphism

Mathematics Subject Classification ID

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

Related Items (1)

Monadic translation of classical sequent calculus

Uses Software

• Unnamed Item

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