Michael J. C. Gordon Professor of Computer Assisted Reasoning The University of Cambridge Computer Laboratory Room FE19, William Gates Building 15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom office: +441223334627, mobile: +447774017428, fax: +441223334678 @ email: mjcg cl.cam.ac.uk

Past research

• Why higher order logic is a good formalism for specifying and verifying hardware
• Mechanizing programming logics in higher order logic
• From LCF to HOL: a short history
• State Transition Assertions (STAs)
• Combining set theory and type theory
• Verilog HDL
• Comparing HOL and PVS
• PROSPER: Proof and Specification Assisted Design Environments
• Christopher Strachey: recollections of his influence
• Formal Specification and Verification of ARM6
• Directions in Formal and Semi-Formal Verification
• Fully Expansive Proof and Algorithmic Verification
• HolBddLib, HolSatLib, puzzleTool
• Deep embedding of Accellera PSL (IBM Sugar 2.0) in HOL
• Programming combinations of deduction and BDD-based symbolic calculation
• STRL Annual Distinguished Seminar
• Invited talk at CAV 2003
• Strachey Lecture
• PSL Semantics in Higher Order Logic (contribution to DCC 2004)
• Translating HOL to hardware
• Linking the HOL4 and ACL2 proof systems
• Mechanically Proving Hoare Formulae (talk given at event celebrating Tony Hoare's 75th birthday)

Teaching

• Temporal Logic and Model Checking
• Hoare Logic
• Programming Logics and Software Verification
• Specification and Verification I (discontinued after 2010)
• Specification and Verification II (discontinued after 2010)
• Introduction to Functional Programming (only of historical interest - last taught in 1996!)
• Student projects (I was the 2008-2009 Part II CST Projects Briefing Officer and Part II Co-ordinator, but these roles passed to David Greaves for 2009-2010 -- instead, I'm now an Examiner!)
• Short talk given to new PhD students on the 2008 Induction Day
• Five minute talk given to potential PhD students on November 18, 2010

Miscellaneous

• Digital clock
• IMMEDIATE ATTENTION NEEDED; costs
• HTML tablemaker, table of HTML characters, HTML validator and WikiFAQ FAQ hosting site
• Google Maps UK, AA Route Planner, Mapquest UK, streetmap.co.uk, Multimap, Mapblast, Mapquest
• Airport taxi services
  • AirportLynx (good, but parking and waiting may put up costs)
  • ECS (excellent: used by Computer Lab and MSR)
  • BATS taxis (never tried, but may be cheap)
• Cambridge University Reporter
• Visitors
• Computer Science Lecture-List timetables
• Term dates
• The Royal Society, and its Fellows
• TTVSI
• Seating posture and adjustment of my office chair
• In praise of thumb-operated trackballs and the ergonomic problems of mice
• What has a snow watching lantern got to do with the HOL88 system?
• Avra Cohn's paper The Notion of Proof in Hardware Verification and her unfinished paper Proof Accounts in HOL
• My first (and last) use of Java applets (from 1996 -- may crash your browser)
• University of Cambridge Library catalogues
• Melatonin for jetlag (NYT, April 30, 1997) and Jetlag Calculator
• TechEncyclopedia
• HTML 4.0 symbols
• Recent projects (needs updating)
• Automated reasoning group home page
• HOL at SourceForge (contains obsolete material)