Skip to content

Commit

Permalink
Merge pull request #232 from jmikedupont2/patch-1
Browse files Browse the repository at this point in the history
removing 404
  • Loading branch information
clarus authored Aug 5, 2024
2 parents d8a5512 + 0d60e98 commit 0912824
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/docs/introduction.md
Original file line number Diff line number Diff line change
Expand Up @@ -83,4 +83,4 @@ In the Rust community:

## Credits
The `coq-of-ocaml` project started as part of a PhD directed by [Yann Regis-Gianas](http://yann.regis-gianas.org/) and [Hugo Herbelin
](http://pauillac.inria.fr/~herbelin/) as the university of [Paris 7](https://u-paris.fr/). Originally, the goal was to formalize real OCaml programs in Coq to study side-effects inference and proof techniques on functional programs. The project is now financed by [Nomadic Labs](https://www.nomadic-labs.com/), with the aim to be able to reason about the implementation of the crypto-currency [Tezos](https://tezos.com/). See this [blog post](http://coq-blog.clarus.me/beginning-of-verification-for-the-parsing-of-smart-contracts.html) to get an example about what we can prove.
](http://pauillac.inria.fr/~herbelin/) as the university of [Paris 7](https://u-paris.fr/). Originally, the goal was to formalize real OCaml programs in Coq to study side-effects inference and proof techniques on functional programs. The project is now financed by [Nomadic Labs](https://www.nomadic-labs.com/), with the aim to be able to reason about the implementation of the crypto-currency [Tezos](https://tezos.com/).

0 comments on commit 0912824

Please sign in to comment.