robur/homepage-data
4
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

.

Browse source
This commit is contained in:
Hannes Mehnert 2017-09-17 00:25:21 +01:00
parent 37e0ff0453
commit fb7e820e4d
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Technology
View file

@ -142,8 +142,7 @@ module interface.
### Verification ### Verification
A large subset of the OCaml semantics has been A large subset of the OCaml semantics has been
[mechanized](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover, and [mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover.
this metatheory is verified.
OCaml is the implementation language of the well-known proof assistant OCaml is the implementation language of the well-known proof assistant
[Coq](https://coq.inria.fr). Development in Coq can be extracted to OCaml code, [Coq](https://coq.inria.fr). Development in Coq can be extracted to OCaml code,