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

Research

• Recent projects (PhD studentship available)
• Automated reasoning group home page
• Cambridge FTP Area for HOL and HOL at SourceForge
• 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
• Combining set theory and type theory
• Verilog HDL and semantics of a small subset
• Comparing HOL and PVS
• PROSPER: Proof and Specification Assisted Design Environments
• Historical talk on work done at Cambridge in the 1980s
• 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

• Specification and Verification I
• Specification and Verification II
• Student projects (I'm the 2008-2009 Part II CST Projects Briefing Officer and Part II Co-ordinator, but for 2009-2010 these roles will pass to David Greaves -- instead, I'll be an Examiner!)
• Short talk given to new PhD students on the 2008 Induction Day

Miscellaneous

• Digital clock
• Borrowing calendar for "hvg" laptop
• When people think of Mike Gordon, I want them to think of a commitment to excellence   :-)
• 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)
• Possibly useful stuff from our December 2005 trip to Seville Spain (now a bit dated)
• Cambridge University Reporter
• Visitors
• Computer Science Lecture-List timetables
• Term dates
• The Royal Society, and its ezine Excellence in Science
• 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)
• Making slides using LaTeX [old method | Beamer].
  Some other methods (I haven't tried most of these, so feedback appreciated):
  • Example presentation using PPower4, an alternative to PowerPoint using LaTeX.
  • TeXPower is another package for making dynamic online presentations with LaTeX.
  • Prosper is a LaTeX class for writing transparencies. Here's an example produced with it
  • TexPoint is a Powerpoint add-in that enables the easy use of Latex symbols and formulas in Powerpoint presentations
  • LaTeX for Logicians by Peter Smith
  • S⁵: A Simple Standards-Based Slide Show System
• University of Cambridge Library catalogues
• Melatonin for jetlag (NYT, April 30, 1997) and Jetlag Calculator
• TechEncyclopedia
• HTML 4.0 symbols