<p>Have you seen Arthur Charguéraud's PhD thesis, <a href="http://www.chargueraud.org/softs/cfml/" rel="noreferrer"><em>Characteristic Formulae for Mechanized Program Verification</em></a>? </p>

<p>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 <code>Obj.magic</code>. To quote from his thesis:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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).</p>

CC BY-SA 3.0
2017-03-01T09:04:12.707Z
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?
Andrea Asperti
CC BY-SA 3.0
2017-03-03T14:34:55.117Z
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?
gasche
CC BY-SA 3.0
2017-03-03T20:08:55.203Z
Strange to have a program that is supposed to certify software and whose behaviour cannot be specififed :)
Andrea Asperti
CC BY-SA 3.0
2017-03-03T21:42:57.587Z
@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.
Martin Berger
CC BY-SA 3.0
2017-03-03T21:54:38.183Z
@MartinBerger I am trying to understand what you get if you apply Chargueraud system to itself, that looks a natural question to me. It should be a CF describing a function that maps programs to CFs. There should be a fixpoint somewhere, right? If you execute an universal machine on an universal machine you still get an universal machine.
Andrea Asperti
CC BY-SA 3.0
2017-03-03T22:02:02.687Z
@AndreaAsperti That is a really interesting question, and I have no idea what the
answer might be. I guess you will reach a fixpoint somehow. But will it be interesting? After all, from the POV of the program constructing the CFs, neither the source nor the target are data types with interseting semantics. It's in some sense just a transfromation from strings (= Ocaml programs) to strings (CFs).
Martin Berger
CC BY-SA 3.0
2017-03-03T22:05:08.250Z
@AndreaAsperti Conincidentally, CFs were not invented by C, they are an old concept from
concurrency theory, cf. [Characteristic Formulae: From Automata to Logic](http://www.brics.dk/RS/07/2/BRICS-RS-07-2.pdf).
CFs where first applied to sequential programming languages by Kohei Honda. Arthur Charguéraud
then took these ideas from theory to practise and actually implemented CFs in Coq and
used them to verify a lot of programs (basically those in Okasaki's on pure functional data structures).
Martin Berger
CC BY-SA 3.0
2017-03-04T02:05:55.163Z
If you have two formal semantics for a language that are expressed in different ways, you can prove that they agree, which tells you something interesting about them -- and builds trust. If you only have one formal semantics, you cannot prove it "correct" as you have no alternative specification. If we had another formal semantics for the subset that CFML support, we could show that the characteristic formula of a program is true for any of its executions in the semantics, which would validate these two semantics against each other.
gasche
CC BY-SA 3.0
2017-03-04T09:51:26.283Z
@gasche The right relation is that the logic is *observationally complete*,
that means that $P$ and $Q$ are contextually indistinguishable iff for
all assertions $A, B$ we have: $\{A\}P\{B\}$ iff $\{A\}Q\{B\}$. In
other words, the axiomatic semantics makes exactly the same
distinctions as the operational semantics. Note that the definition of
observationally completeness leave it open whether the meaning of a program
can always be captured by a single pair of assertions. CFs have the additional property that the semantics of a program is captured in a *single* pre/post-condition pair.
Martin Berger
CC BY-SA 3.0
2017-03-04T09:52:06.580Z
@Neel Krishnaswami In what sense is the meta-theory of CFs uninteresting?
Martin Berger
CC BY-SA 3.0
2017-03-05T14:01:59.973Z
@gashe But, in principle, it should be possible to prove the correctness of the system at least with respect to its own semantic specification, that is the "fixpoint"I was talking about. CF(S) is essentially a map from programs to CFs, so I would expect to have an equivalence between CF(S) and CF(S)@S, if you see what I mean.
Andrea Asperti
CC BY-SA 3.0
2017-03-06T10:56:22.883Z
@MartinBerger: I meant Arthur's CFML tool, not CFs in general. There is a lot more work to do to establish the metatheoretic properties of the tool itself. (In his thesis Arthur did a pen-and-paper proof for a small ML-like language, not Ocaml proper.) However, I recently found out that one of his students and the CakeML people have done a mechanized correctness proof of a CF-based proof system for CakeML, which goes all the way to verified machine code! (ESOP 2017: Armaël Guéneau, Magnus O. Myreen, Ramana Kumar and Michael Norrish, *Verified Characteristic Formulae for CakeML*.)
Neel Krishnaswami
CC BY-SA 3.0
2017-03-06T14:32:34.227Z
@NeelKrishnaswami The CakeML is amazing. Interestingly the Guéneau et al paper proves only soundness, not CF-ness, i.e. whether the derived pre/post-conditions in fact characterise the programs they derive from. I wonder why.
Martin Berger
CC BY-SA 3.0
2017-03-07T17:06:57.723Z
@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.)
Neel Krishnaswami
CC BY-SA 3.0
2017-02-28T12:01:04.570Z
2017-02-28T12:01:04.570Z
Neel Krishnaswami
<p>You could be interested in Jacques Garrigue's <a href="https://www.math.nagoya-u.ac.jp/~garrigue/papers/aplas2010.html" rel="noreferrer">A Certified Implementation of ML with Structural Polymorphism and Recursive Types</a>, which establishes the soundness of static and dynamic semantics <em>and</em> 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).</p>

<p>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.</p>

CC BY-SA 3.0
2017-03-03T14:34:02.297Z
2017-03-03T14:34:02.297Z
gasche
<p>The semantics of a large subset of OCaml, called <a href="http://dl.acm.org/citation.cfm?id=1792880" rel="nofollow noreferrer">OCamllight</a>,  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 <a href="http://www.cs.cornell.edu/jyh/papers/cade15_pe/paper.pdf" rel="nofollow noreferrer">Kreitz, Hayden and Hickey</a>. </p>

<p>Is there any similar development in Coq?</p>

CC BY-SA 4.0
2019-02-04T18:04:55.733Z
You might be interested in CakeML : https://cakeml.org/. I'ts not OCaml specifically, though.
Joey Eremondi
<coq><program-verification><ocaml>
Formal semantics of OCaml in Coq
Andrea Asperti
# Formal semantics of OCaml in Coq

(Asked by: username_0 on 2017-02-28)

The semantics of a large subset of OCaml, called [OCamllight](http://dl.acm.org/citation.cfm?id=1792880), 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](http://www.cs.cornell.edu/jyh/papers/cade15_pe/paper.pdf).

Is there any similar development in Coq?

**Tags:** coq, program-verification, ocaml
> **Comments:**
> **username_1**: You might be interested in CakeML : https://cakeml.org/. I'ts not OCaml specifically, though.  

---

## 2 answers

### Answer by username_2 on 2017-02-28. Score: 12

Have you seen Arthur Charguéraud's PhD thesis, [*Characteristic Formulae for Mechanized Program Verification*](http://www.chargueraud.org/softs/cfml/)?

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).

> **Comments:**
> **username_0**: 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?  
> **username_3**: 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?  
> **username_0**: Strange to have a program that is supposed to certify software and whose behaviour cannot be specififed :)  
> **username_4**: @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.  
> **username_0**: @MartinBerger I am trying to understand what you get if you apply Chargueraud system to itself, that looks a natural question to me. It should be a CF describing a function that maps programs to CFs. There should be a fixpoint somewhere, right? If you execute an universal machine on an universal machine you still get an universal machine.  
> **username_4**: @AndreaAsperti That is a really interesting question, and I have no idea what the answer might be. I guess you will reach a fixpoint somehow. But will it be interesting? After all, from the POV of the program constructing the CFs, neither the source nor the target are data types with interseting semantics. It's in some sense just a transfromation from strings (= Ocaml programs) to strings (CFs).  
> **username_4**: @AndreaAsperti Conincidentally, CFs were not invented by C, they are an old concept from concurrency theory, cf. [Characteristic Formulae: From Automata to Logic](http://www.brics.dk/RS/07/2/BRICS-RS-07-2.pdf). CFs where first applied to sequential programming languages by Kohei Honda. Arthur Charguéraud then took these ideas from theory to practise and actually implemented CFs in Coq and used them to verify a lot of programs (basically those in Okasaki's on pure functional data structures).  
> **username_3**: If you have two formal semantics for a language that are expressed in different ways, you can prove that they agree, which tells you something interesting about them -- and builds trust. If you only have one formal semantics, you cannot prove it "correct" as you have no alternative specification. If we had another formal semantics for the subset that CFML support, we could show that the characteristic formula of a program is true for any of its executions in the semantics, which would validate these two semantics against each other.  
> **username_4**: @gasche The right relation is that the logic is *observationally complete*, that means that $P$ and $Q$ are contextually indistinguishable iff for all assertions $A, B$ we have: $\{A\}P\{B\}$ iff $\{A\}Q\{B\}$. In other words, the axiomatic semantics makes exactly the same distinctions as the operational semantics. Note that the definition of observationally completeness leave it open whether the meaning of a program can always be captured by a single pair of assertions. CFs have the additional property that the semantics of a program is captured in a *single* pre/post-condition pair.  
> **username_4**: @Neel Krishnaswami In what sense is the meta-theory of CFs uninteresting?  
> **username_0**: @gashe But, in principle, it should be possible to prove the correctness of the system at least with respect to its own semantic specification, that is the "fixpoint"I was talking about. CF(S) is essentially a map from programs to CFs, so I would expect to have an equivalence between CF(S) and CF(S)@S, if you see what I mean.  
> **username_2**: @MartinBerger: I meant Arthur's CFML tool, not CFs in general. There is a lot more work to do to establish the metatheoretic properties of the tool itself. (In his thesis Arthur did a pen-and-paper proof for a small ML-like language, not Ocaml proper.) However, I recently found out that one of his students and the CakeML people have done a mechanized correctness proof of a CF-based proof system for CakeML, which goes all the way to verified machine code! (ESOP 2017: Armaël Guéneau, Magnus O. Myreen, Ramana Kumar and Michael Norrish, *Verified Characteristic Formulae for CakeML*.)  
> **username_4**: @NeelKrishnaswami The CakeML is amazing. Interestingly the Guéneau et al paper proves only soundness, not CF-ness, i.e. whether the derived pre/post-conditions in fact characterise the programs they derive from. I wonder why.  
> **username_2**: @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.)  

---

### Answer by username_3 on 2017-03-03. Score: 8

You could be interested in Jacques Garrigue's [A Certified Implementation of ML with Structural Polymorphism and Recursive Types](https://www.math.nagoya-u.ac.jp/~garrigue/papers/aplas2010.html), 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.


---

