Robert S. Boyer
Edward A. Lee
Natarajan Shankar
Thierry Viéville
Proof systems
Automated Reasoning System Implementations
(
Europe mirror
)
User Interface for Theorem Provers
PVS
Jape
Coq
NuPrl
TkHol
Porgi
ORA Canada
Graphical tools
Koala
companies
Ilog
Simulog