A Church-style intermediate language for ML^ F

DOI10.1016/J.TCS.2012.02.026MaRDI QIDQ428892zbMATH OpenOpenAlexFDO

Authors Didier Rémy, Boris Yakobowski

Publication date 25 June 2012

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

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

zbMATH Keywords

binderscoercionsML\(^{\text F}\)retyping functionsSystem Ftype generalizationtype instantiationtype soundnesstypes

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• A church-style intermediate language for ML\(^{\text{F}}\)
• Towards an intersection typed system à la Church
• The ML approach to the readable all-purpose language
• Church-Rosser systems with respect to formal languages
• Compiling a functional logic language: \textit{The Fair Scheme}
• Sequent calculus as a compiler intermediate language
• Implicit typing à la ML for the join-calculus
• scientific article; zbMATH DE number 1956524

Cites work

• A theory of qualified types
• A type directed translation of MLF to System F
• Engineering formal metatheory
• From ML to ML ^F
• Generative type abstraction and type-level computation
• Harnessing \(\mathrm{ML}^{\mathrm F}\) with the power of system F
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• ML ^F
• Polymorphic type inference and containment
• Qualified types for MLF
• Recasting ML\(^{\text F}\)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Typed compilation of inclusive subtyping

Cited in

(4)

• Recasting ML\(^{\text F}\)
• A church-style intermediate language for ML\(^{\text{F}}\)
• Harnessing \(\mathrm{ML}^{\mathrm F}\) with the power of system F
• A type directed translation of MLF to System F

Describes a project that uses

Uses Software

• Haskell
• Coq

This page was built for publication: A Church-style intermediate language for ML\(^{\text F}\)

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