A certified implementation of ML with structural polymorphism and recursive types

DOI10.1017/S0960129513000066zbMath1361.68038OpenAlexW2110685049MaRDI QIDQ5740642

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)

Related Items (1)

No value restriction is needed for algebraic effects and handlers

Uses Software

• OCaml
• Unnamed Item

Cites Work

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

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