Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions

DOI10.1016/j.tcs.2011.05.051zbMath1238.03029OpenAlexW2154331311MaRDI QIDQ764331

Paolo Tranquilli, Giulio Manzonetto

Publication date: 13 March 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.05.051

zbMATH Keywords

strong normalization\(\mathsf{ML}^{\mathsf F}\)\(\mathsf{xML}^{\mathsf F}\)calculus of coercionspolymorphic types

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• ML
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• Light types for polynomial time computation in lambda calculus
• Recasting ML\(^{\text F}\)
• The lambda calculus, its syntax and semantics
• A theory of type polymorphism in programming
• Typability and type checking in System F are equivalent and undecidable
• An extension of system \(F\) with subtyping
• Termination of system \(F\)-bounded: A complete proof
• Typed compilation of inclusive subtyping
• Harnessing ML F with the Power of System F
• A type directed translation of MLF to system F
• ML ^F
• Intensional interpretations of functionals of finite type I