Archives of the Caml mailing list > Message from Jean-Christophe Filliatre

Browse thread

Programming with correctness guarantees

oleg@p...
- Andrej Bauer
  - Chris King
    - Jean-Christophe Filliatre
- Joshua D. Guttman
  - Jean-Christophe Filliatre
    - Robert Fischer
      - Jean-Christophe Filliatre
        
        skaller
    - Jacques Carette
      - Bob Williams
- Jean-Christophe Filliatre
  - Tom
- David MENTRE

Date:	-- (:)
From:	Jean-Christophe Filliatre <filliatr@l...>
Subject:	Re: [Caml-list] Programming with correctness guarantees


 > > it would be interesting to augment real programming
 > > languages with ways of writing specifications that can then be tackled
 > > by theorem provers and proof asistants.

Some readers of this thread may be interested by the following proof
of an OCaml implementation of Peterson's algorithm by Tom Ridge:

http://www.cl.cam.ac.uk/~tjr22/doc/concTalk20070124.pdf

-- 
Jean-Christophe