Strong normalization of ML^ F via a calculus of coercions

DOI10.1016/J.TCS.2011.05.051MaRDI QIDQ764331zbMATH OpenOpenAlexFDO

Authors Giulio Manzonetto, Paolo Tranquilli

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

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

Mathematics Subject Classification ID

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

Recommendations

• Foundations of Software Science and Computation Structures
• Strong normalisation in the \(\pi\)-calculus
• scientific article; zbMATH DE number 1555189
• Functional and Logic Programming
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• scientific article; zbMATH DE number 2080223
• Strong normalization of \(\lambda^{\mathrm{Sym}}_{\mathrm{Prop}}\)- and \(\overline{\lambda}\mu\overline{\mu}^\ast\)-calculi
• Strong normalizability as a finiteness structure via the Taylor expansion of -terms
• Strong Normalization and Equi-(Co)Inductive Types

Cites work

• A theory of type polymorphism in programming
• A type directed translation of MLF to System F
• An extension of system \(F\) with subtyping
• Harnessing \(\mathrm{ML}^{\mathrm F}\) with the power of system F
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Light types for polynomial time computation in lambda calculus
• Linear logic
• ML ^F
• Recasting ML\(^{\text F}\)
• Termination of system F-bounded: A complete proof
• The lambda calculus, its syntax and semantics
• Typability and type checking in System F are equivalent and undecidable
• Typed compilation of inclusive subtyping

Cited in

(4)

• A church-style intermediate language for ML\(^{\text{F}}\)
• Harnessing \(\mathrm{ML}^{\mathrm F}\) with the power of system F
• scientific article; zbMATH DE number 512769 (Why is no real title available?)
• System F with coercion constraints

Describes a project that uses

Uses Software

• ML
• Automath

This page was built for publication: Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions

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