A Church-style intermediate language for ML^ F
DOI10.1016/J.TCS.2012.02.026zbMATH Open1252.03080OpenAlexW2168533104MaRDI QIDQ428892FDOQ428892
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
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
typesbinderscoercionsML\(^{\text F}\)retyping functionsSystem Ftype generalizationtype instantiationtype soundness
Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)
Cites Work
- Title not available (Why is that?)
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Recasting ML\(^{\text F}\)
- Polymorphic type inference and containment
- A theory of qualified types
- Qualified types for MLF
- Typed compilation of inclusive subtyping
- Engineering formal metatheory
- Harnessing \(\mathrm{ML}^{\mathrm F}\) with the power of system F
- A type directed translation of MLF to System F
- From ML to ML F
- ML F
- Generative type abstraction and type-level computation
Cited In (4)
Uses Software
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)