- A proof of a distributed reference counting algorithm in Coq Distributed Algorithm

- Home page of John Harrison, doing formal verification of software ar Intel Corporation Among other things, he has formalised Dijkstra's book in HOL Harrison

- Helmut Schwichtenberg has carried out interesting examples of program extractions using the system Minlog Schwichtenberg

- Proof Animation, a nonstandard use of Curry-Howard, by Susumu Hayashi Proof Animation

- Home Page of Martin Hofmann, presenting some Polynomial Time Type Systems Hofmann

Last modified: Fri Sep 17 20:48:44 MET DST 1999