Michael J. C. Gordon

Publication Activity (10 Years)

Years Active: 1978-2012
Publications (10 Years): 0

Top Venues

Sci. Comput. Program.

FMCAD

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Decompilation into logic - Improved. FMCAD (2012)
Magnus O. Myreen, Michael J. C. Gordon
Function extraction. Sci. Comput. Program. 77 (4) (2012)
Michael J. C. Gordon, Matt Kaufmann, Sandip Ray
The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. J. Autom. Reason. 47 (1) (2011)
Michael J. C. Gordon
ML: metalanguage or object language? ICFP (2010)
Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
Extensible Proof-Producing Compilation. CC (2009)
Magnus O. Myreen, Michael J. C. Gordon
Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs (2009)
Magnus O. Myreen, Michael J. C. Gordon
Transforming Programs into Recursive Functions. Electron. Notes Theor. Comput. Sci. 240 (2009)
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD (2008)
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
Hoare Logic for ARM Machine Code. FSEN (2007)
Magnus O. Myreen, Michael J. C. Gordon
Hoare Logic for Realistically Modelled Machine Code. TACAS (2007)
Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
An embedding of the ACL2 logic in HOL. ACL2 (2006)
Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
An Integration of HOL and ACL2. FMCAD (2006)
Michael J. C. Gordon, Joe Hurd, Konrad Slind
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. CHARME (2003)
Michael J. C. Gordon
Validating the PSL/Sugar Semantics Using Automated Reasoning. Formal Aspects Comput. 15 (4) (2003)
Michael J. C. Gordon
Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45 (1) (2002)
Michael J. C. Gordon
PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs (2002)
Michael J. C. Gordon
Christopher Strachey: Recollections of His Influence. High. Order Symb. Comput. 13 (1/2) (2000)
Michael J. C. Gordon
Reachability Programming in HOL98 Using BDDs. TPHOLs (2000)
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)
Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy
M and HOL. CADE (1998)
Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon
An Interface between Clam and HOL. TPHOLs (1998)
Michael J. C. Gordon
Set Theory, Higher Order Logic or Both? TPHOLs (1996)
Michael J. C. Gordon
The Semantic Challenge of Verilog HDL LICS (1995)
Sten Agerholm, Michael J. C. Gordon
Experiments with ZF Set Theory in HOL and Isabelle. TPHOLs (1995)
Jonathan P. Bowen, Michael J. C. Gordon
Z and HOL. Z User Workshop (1994)
Michael J. C. Gordon
A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). CAV (1993)
Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel
Experience with Embedding Hardware Description Languages in HOL. TPCD (1992)
Michael J. C. Gordon
Introduction to the HOL System. TPHOLs (1991)
C. A. R. Hoare, Michael J. C. Gordon
Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic LICS (1988)
Michael J. C. Gordon
The Denotational Semantics of Sequential Machines. Inf. Process. Lett. 10 (1) (1980)
Michael J. C. Gordon
On the Power of List Iteration. Comput. J. 22 (4) (1979)
Michael J. C. Gordon, Robin Milner, L. Morris, Malcolm C. Newey, Christopher P. Wadsworth
A Metalanguage for Interactive Proof in LCF. POPL (1978)

Michael J. C. Gordon.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Michael J. C. Gordon