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 |