A certified implementation of ML with structural polymorphism and recursive types

DOI10.1017/S0960129513000066MaRDI QIDQ5740642zbMATH OpenOpenAlexFDO

Authors Jacques Garrigue

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129513000066

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Recommendations

• Certification of a type inference tool for ML: Damas-Milner within Coq
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 1670740
• Extending the type checker of Standard ML by polymorphic recursion
• A Sound Semantics for OCaml light

Cites work

• A Sound Semantics for OCaml light
• Certification of a type inference tool for ML: Damas-Milner within Coq
• Semi-explicit first-class polymorphism for ML.
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Verifying the unification algorithm in LCF

Cited in

(2)

• Certification of a type inference tool for ML: Damas-Milner within Coq
• No value restriction is needed for algebraic effects and handlers

Describes a project that uses

Uses Software

• OCaml
• Coq

This page was built for publication: A certified implementation of ML with structural polymorphism and recursive types

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