Evaluation and denotation of pure LISP programs : a worked example in semantics. - Michael J. C. Gordon (1974)

A Metalanguage for Interactive Proof in LCF. - Michael J. C. Gordon; Robin Milner; F. Lockwood Morris; Malcolm C. Newey; Christopher P. Wadsworth (POPL, 1978)

The denotational description of programming languages - an introduction. - Michael J. C. Gordon (Springer, 1979)

Edinburgh LCF - Michael J. C. Gordon; Robin Milner; Christopher P. Wadsworth (Springer, 1979)

On the Power of List Iteration. - Michael J. C. Gordon (Comput. J., 1979)

The Denotational Semantics of Sequential Machines. - Michael J. C. Gordon (Inf. Process. Lett., 1980)

Programming language theory and its implementation - applicative and imperative paradigms. - Michael J. C. Gordon (Prentice Hall, 1988)

Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic - C. A. R. Hoare; Michael J. C. Gordon (LICS, 1988)

Introduction to the HOL System. - Michael J. C. Gordon (TPHOLs, 1991)

Experience with Embedding Hardware Description Languages in HOL. - Richard J. Boulton; Andrew D. Gordon 001; Michael J. C. Gordon; John Harrison 001; John Herbert; John Van Tassel (TPCD, 1992)

A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). - Michael J. C. Gordon (CAV, 1993)

Z and HOL. - Jonathan P. Bowen; Michael J. C. Gordon (Z User Workshop, 1994)

The Semantic Challenge of Verilog HDL - Michael J. C. Gordon (LICS, 1995)

Experiments with ZF Set Theory in HOL and Isabelle. - Sten Agerholm; Michael J. C. Gordon (TPHOLs, 1995)

A shallow embedding of Z in HOL. - Jonathan P. Bowen; Mike Gordon (Inf. Softw. Technol., 1995)

Set Theory, Higher Order Logic or Both? - Michael J. C. Gordon (TPHOLs, 1996)

System Description: An Interface Between CLAM and HOL. - Konrad Slind; Michael J. C. Gordon; Richard J. Boulton; Alan Bundy (CADE, 1998)

An Interface between Clam and HOL. - Richard J. Boulton; Konrad Slind; Alan Bundy; Michael J. C. Gordon (TPHOLs, 1998)

From LCF to HOL: a short history. - Mike Gordon (Proof, Language, and Interaction, 2000)

The PROSPER Toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Graham Robinson; Michael J. C. Gordon; Thomas F. Melham (TACAS, 2000)

Reachability Programming in HOL98 Using BDDs. - Michael J. C. Gordon (TPHOLs, 2000)

Christopher Strachey: Recollections of His Influence. - Michael J. C. Gordon (High. Order Symb. Comput., 2000)

PuzzleTool : An Example of Programming Computation and Deduction. - Michael J. C. Gordon (TPHOLs, 2002)

Relating Event and Trace Semantics of Hardware Description Languages. - Michael J. C. Gordon (Comput. J., 2002)

Programming Combinations of Deduction and BDD-based Symbolic Calculation. - Michael J. C. Gordon (LMS J. Comput. Math., 2002)

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. - Michael J. C. Gordon; Joe Hurd; Konrad Slind (CHARME, 2003)

Validating the PSL/Sugar Semantics Using Automated Reasoning. - Michael J. C. Gordon (Formal Aspects Comput., 2003)

Automatic Formal Synthesis of Hardware from Higher Order Logic. - Mike Gordon; Juliano Iyoda; Scott Owens; Konrad Slind (AVoCS, 2005)

An embedding of the ACL2 logic in HOL. - Michael J. C. Gordon; Warren A. Hunt Jr.; Matt Kaufmann; James Reynolds (ACL2, 2006)

An Integration of HOL and ACL2. - Michael J. C. Gordon; James Reynolds; Warren A. Hunt Jr.; Matt Kaufmann (FMCAD, 2006)

Model Checking PSL Using HOL and SMV. - Thomas Tuerk; Klaus Schneider 001; Mike Gordon (Haifa Verification Conference, 2006)

Hoare Logic for ARM Machine Code. - Magnus O. Myreen; Anthony C. J. Fox; Michael J. C. Gordon (FSEN, 2007)

Hoare Logic for Realistically Modelled Machine Code. - Magnus O. Myreen; Michael J. C. Gordon (TACAS, 2007)

Proof producing synthesis of arithmetic and cryptographic hardware. - Konrad Slind; Scott Owens; Juliano Iyoda; Mike Gordon (Formal Aspects Comput., 2007)

Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. - Magnus O. Myreen; Michael J. C. Gordon; Konrad Slind (FMCAD, 2008)

Twenty Years of Theorem Proving for HOLs Past, Present and Future. - Mike Gordon (TPHOLs, 2008)

Transforming Programs into Recursive Functions. - Magnus O. Myreen; Michael J. C. Gordon (SBMF, 2008)

Extensible Proof-Producing Compilation. - Magnus O. Myreen; Konrad Slind; Michael J. C. Gordon (CC, 2009)

Verified LISP Implementations on ARM, x86 and PowerPC. - Magnus O. Myreen; Michael J. C. Gordon (TPHOLs, 2009)

Forward with Hoare. - Mike Gordon; Hélène Collavizza (Reflections on the Work of C. A. R. Hoare, 2010)

Specification and Verification of ARM Hardware and Software. - Anthony C. J. Fox; Michael J. C. Gordon; Magnus O. Myreen (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

ML: metalanguage or object language? - Michael J. C. Gordon (ICFP, 2010)

The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. - Michael J. C. Gordon; Matt Kaufmann; Sandip Ray (J. Autom. Reason., 2011)

Decompilation into logic - Improved. - Magnus O. Myreen; Michael J. C. Gordon; Konrad Slind (FMCAD, 2012)

Function extraction. - Magnus O. Myreen; Michael J. C. Gordon (Sci. Comput. Program., 2012)