14
$\begingroup$

The semantics of a large subset of OCaml, called OCamllight, was formalized in HOL by Owens several years ago. More recently, a type theoretical semantics of a smaller subset of OCaml was implemented in Nuprl by Kreitz, Hayden and Hickey.

Is there any similar development in Coq?

Improve this question
$\endgroup$
1
  • $\begingroup$ You might be interested in CakeML : cakeml.org. I'ts not OCaml specifically, though. $\endgroup$
    – Joey Eremondi
    Commented Feb 4, 2019 at 18:04

2 Answers 2

Reset to default
12
$\begingroup$

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 gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a very large subset of Ocaml -- notably, including unsafe casts like Obj.magic. To quote from his thesis:

I have focused on a subset of the OCaml programming lan- guage, which is a sequential, call-by-value, high-level programming language. The current implementation of CFML supports the core λ-calculus, including higher- order functions, recursion, mutual recursion and polymorphic recursion. It supports tuples, data constructors, pattern matching, reference cells, records and arrays. I provide an additional Caml library that adds support for null pointers and strong updates.

It's a very appealing approach if you want to prove a particular Caml program correct (less so if you are interested in its metatheory, though).

Improve this answer
$\endgroup$
14
  • $\begingroup$ So, if I understand right, the specification of the semantics of Ocaml is embedded in the system. Is it possible to interpret the characteristic formula of (some key function of the) system as such a specification? Also, I presume the system is written in OCaml. Is it possible to specify and prove its correctness in the system itself? $\endgroup$
    – Andrea Asperti
    Commented Mar 1, 2017 at 9:04
  • $\begingroup$ For a given OCaml program, its characteristic formula can be thought of a denotational semantics, a "least general" specification that can be used to prove any desirable properties of the program. If you speak of the "correctness" of CFML itself, the question is: with respect to which alternative formal semantics? $\endgroup$
    – gasche
    Commented Mar 3, 2017 at 14:34
  • $\begingroup$ Strange to have a program that is supposed to certify software and whose behaviour cannot be specififed :) $\endgroup$
    – Andrea Asperti
    Commented Mar 3, 2017 at 20:08
  • $\begingroup$ @AndreaAsperti What do you mean by "embedded in the system"? The idea behind characteristic formulae (CFs) is quite straightforward: map programs to logical formulae (typically pre- and postcondition) such the formulae precisely describe the semantics of the programs. In other words two programs satisfy the same CFs iff they are contextually indistinguishable. The map from program to CFs is done by induction of the structure of the program, and can target any sufficiently expressive logic. A. Charguéraud target's Coq's logic, but that's a contingent choice. $\endgroup$
    – Martin Berger
    Commented Mar 3, 2017 at 21:42
  • 1
    $\begingroup$ @MartinBerger: the Guéneau et al paper only proves soundness because the derived pre/posts don't characterize the programs they derive from. Their CFs are derived from the untyped semantics of CakeML, but the typed language has a different observational equivalence. (For practical verification, this isn't terribly important, and it's easier.) $\endgroup$
    – Neel Krishnaswami
    Commented Mar 7, 2017 at 17:06
8
$\begingroup$

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 properties of type inference for a ML language with (recursion and) structural polymorphism, thus formalizing one of the more advanced corners of OCaml (polymorphic variants and object types).

That said, this work is more aimed at verifying soundness of more advanced parts of the type system than at covering the feature set of existing OCaml programs. I think that in terms of trying to prove correctness of an existing OCaml program, CFML would be a better choice.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.