Some Sites on Interactive Proof Systems

• PVS home page

• Some papers on formal methods

• Logical Frameworks

• Coq

• 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

• Theorema