A Church-style intermediate language for ML^ F
DOI10.1016/J.TCS.2012.02.026zbMATH Open1252.03080OpenAlexW2168533104MaRDI QIDQ428892FDOQ428892
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
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 ML 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
Uses Software
Recommendations
- A Church-Style Intermediate Language for ML 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: The Fair Scheme π π
- Sequent calculus as a compiler intermediate language π π
- Implicit typing Γ la ML for the join-calculus π π
- Title not available (Why is that?) π π
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)