Skip to main content
12 votes

Formal semantics of OCaml in Coq

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he ...
Neel Krishnaswami's user avatar
8 votes

Formal semantics of OCaml in Coq

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...
gasche's user avatar
  • 2,040
4 votes

Why does ML's Value Restriction stop you from capturing parametric values?

Your C# example doesn't trigger the value restriction at all. Here it is in OCaml: ...
Drup's user avatar
  • 141
2 votes
Accepted

Why does ML's Value Restriction stop you from capturing parametric values?

However, I can easily make a C# function which captures a parameterized variable, and parametrically instantiate it over both int and string. The equivalent to code forbidden by value restriction ...
Alexey Romanov's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible