Professor of Computational Logic
Computer Laboratory, University of Cambridge, UK
|
Submit a paper to JCM! | ||||||||
| Publications and Grants | |||||||||
| Isabelle prover and list of Projects | |
||||||||
| Curriculum Vitae | |||||||||
| The book ML for the Working Programmer | |
||||||||
| $2.56 | |||||||||
My research concerns interactive theorem proving and its applications:
The Isabelle system is a popular generic theorem prover, developed in collaboration with Tobias Nipkow and his colleagues at T. U. Munich. During the 1980s, my work on LCF introduced concepts such as conversions and theorem continuations, which are still mainstays of the HOL system. I was involved in the design of the programming language Standard ML and have written one of the main textbooks, ML for the Working Programmer. Recent research grants concern temporal reasoning and verification of cryptographic protocols.
I am a Fellow of Clare College.
Usage statistics for my pages are available, and various downloads. I have also built another site.
| Computer Laboratory, University of Cambridge, England |
Telephone: (01223) 334623 Fax: (01223) 334678 E-mail: lcp@cl.cam.ac.uk |
PGP : D8 A7 F0 F4 0B FE 38 DB 2B CF 7C 8C 6A 1A 3E 04