A Church-style intermediate language for ML\(^{\text F}\)

DOI10.1016/J.TCS.2012.02.026zbMath1252.03080OpenAlexW2168533104MaRDI QIDQ428892

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

typesbinderscoercionsML\(^{\text F}\)retyping functionsSystem Ftype generalizationtype instantiationtype soundness

Mathematics Subject Classification ID

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

Uses Software

• Haskell
• Unnamed Item

Cites Work

• Unnamed Item
• 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

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