| 2009 |
|---|
| 27 | EE | Magnus O. Myreen,
Konrad Slind,
Michael J. C. Gordon:
Extensible Proof-Producing Compilation.
CC 2009: 2-16 |
| 2007 |
|---|
| 26 | EE | Magnus O. Myreen,
Anthony C. J. Fox,
Michael J. C. Gordon:
Hoare Logic for ARM Machine Code.
FSEN 2007: 272-286 |
| 25 | EE | Magnus O. Myreen,
Michael J. C. Gordon:
Hoare Logic for Realistically Modelled Machine Code.
TACAS 2007: 568-582 |
| 2006 |
|---|
| 24 | EE | Michael J. C. Gordon,
Warren A. Hunt Jr.,
Matt Kaufmann,
James Reynolds:
An embedding of the ACL2 logic in HOL.
ACL2 2006: 40-46 |
| 23 | EE | Michael J. C. Gordon,
James Reynolds,
Warren A. Hunt Jr.,
Matt Kaufmann:
An Integration of HOL and ACL2.
FMCAD 2006: 153-160 |
| 2003 |
|---|
| 22 | EE | Michael J. C. Gordon,
Joe Hurd,
Konrad Slind:
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.
CHARME 2003: 200-215 |
| 21 | EE | Michael J. C. Gordon:
Validating the PSL/Sugar Semantics Using Automated Reasoning.
Formal Asp. Comput. 15(4): 406-421 (2003) |
| 2002 |
|---|
| 20 | EE | Michael J. C. Gordon:
PuzzleTool : An Example of Programming Computation and Deduction.
TPHOLs 2002: 214-229 |
| 19 | EE | Michael J. C. Gordon:
Relating Event and Trace Semantics of Hardware Description Languages.
Comput. J. 45(1): 27-36 (2002) |
| 2000 |
|---|
| 18 | EE | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Graham Robinson,
Michael J. C. Gordon,
Thomas F. Melham:
The PROSPER Toolkit.
TACAS 2000: 78-92 |
| 17 | | Michael J. C. Gordon:
Reachability Programming in HOL98 Using BDDs.
TPHOLs 2000: 179-196 |
| 16 | | Michael J. C. Gordon:
Christopher Strachey: Recollections of His Influence.
Higher-Order and Symbolic Computation 13(1/2): 65-67 (2000) |
| 1998 |
|---|
| 15 | EE | Konrad Slind,
Michael J. C. Gordon,
Richard J. Boulton,
Alan Bundy:
System Description: An Interface Between CLAM and HOL.
CADE 1998: 134-138 |
| 14 | | Richard J. Boulton,
Konrad Slind,
Alan Bundy,
Michael J. C. Gordon:
An Interface between Clam and HOL.
TPHOLs 1998: 87-104 |
| 1996 |
|---|
| 13 | | Michael J. C. Gordon:
Set Theory, Higher Order Logic or Both?
TPHOLs 1996: 191-201 |
| 1995 |
|---|
| 12 | | Michael J. C. Gordon:
The Semantic Challenge of Verilog HDL
LICS 1995: 136-145 |
| 11 | | Sten Agerholm,
Michael J. C. Gordon:
Experiments with ZF Set Theory in HOL and Isabelle.
TPHOLs 1995: 32-45 |
| 1994 |
|---|
| 10 | | Jonathan P. Bowen,
Michael J. C. Gordon:
Z and HOL.
Z User Workshop 1994: 141-167 |
| 1993 |
|---|
| 9 | | Luc J. M. Claesen,
Michael J. C. Gordon:
Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992
North-Holland/Elsevier 1993 |
| 8 | | Michael J. C. Gordon:
A Verifier and Timing Analyser for Simple Imperative Programs (Abstract).
CAV 1993: 320 |
| 1992 |
|---|
| 7 | | Richard J. Boulton,
Andrew Gordon,
Michael J. C. Gordon,
John Harrison,
John Herbert,
John Van Tassel:
Experience with Embedding Hardware Description Languages in HOL.
TPCD 1992: 129-156 |
| 1991 |
|---|
| 6 | | Michael J. C. Gordon:
Introduction to the HOL System.
TPHOLs 1991: 2-3 |
| 1988 |
|---|
| 5 | | C. A. R. Hoare,
Michael J. C. Gordon:
Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic
LICS 1988: 28-36 |
| 1980 |
|---|
| 4 | | Michael J. C. Gordon:
The Denotational Semantics of Sequential Machines.
Inf. Process. Lett. 10(1): 1-3 (1980) |
| 1979 |
|---|
| 3 | | Michael J. C. Gordon,
Robin Milner,
Christopher P. Wadsworth:
Edinburgh LCF
Springer 1979 |
| 2 | | Michael J. C. Gordon:
On the Power of List Iteration.
Comput. J. 22(4): 376-379 (1979) |
| 1978 |
|---|
| 1 | | Michael J. C. Gordon,
Robin Milner,
L. Morris,
Malcolm C. Newey,
Christopher P. Wadsworth:
A Metalanguage for Interactive Proof in LCF.
POPL 1978: 119-130 |
