Michael J. C. Gordon

Magnus O. Myreen, Michael J. C. Gordon: Function extraction. Sci. Comput. Program. 77(4): 505-517 (2012)

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind: Decompilation into logic - Improved. FMCAD 2012: 78-81

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. Reasoning 47(1): 1-16 (2011)

Michael J. C. Gordon: ML: metalanguage or object language? ICFP 2010: 1-2

Magnus O. Myreen, Michael J. C. Gordon: Transforming Programs into Recursive Functions. Electr. Notes Theor. Comput. Sci. 240: 185-200 (2009)

Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon: Extensible Proof-Producing Compilation. CC 2009: 2-16

Magnus O. Myreen, Michael J. C. Gordon: Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs 2009: 359-374

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

Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon: Hoare Logic for ARM Machine Code. FSEN 2007: 272-286

Magnus O. Myreen, Michael J. C. Gordon: Hoare Logic for Realistically Modelled Machine Code. TACAS 2007: 568-582

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

Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160

Michael J. C. Gordon: Validating the PSL/Sugar Semantics Using Automated Reasoning. Formal Asp. Comput. 15(4): 406-421 (2003)

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

Michael J. C. Gordon: Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45(1): 27-36 (2002)

Michael J. C. Gordon: PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs 2002: 214-229

Michael J. C. Gordon: Christopher Strachey: Recollections of His Influence. Higher-Order and Symbolic Computation 13(1/2): 65-67 (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: 78-92

Michael J. C. Gordon: Reachability Programming in HOL98 Using BDDs. TPHOLs 2000: 179-196

Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy: System Description: An Interface Between CL^AM and HOL. CADE 1998: 134-138

Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon: An Interface between Clam and HOL. TPHOLs 1998: 87-104

Michael J. C. Gordon: Set Theory, Higher Order Logic or Both? TPHOLs 1996: 191-201

Michael J. C. Gordon: The Semantic Challenge of Verilog HDL. LICS 1995: 136-145

Sten Agerholm, Michael J. C. Gordon: Experiments with ZF Set Theory in HOL and Isabelle. TPHOLs 1995: 32-45

Jonathan P. Bowen, Michael J. C. Gordon: Z and HOL. Z User Workshop 1994: 141-167

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

Luc J. M. Claesen, Michael J. C. Gordon (Eds.): Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992. IFIP Transactions A-20, North-Holland/Elsevier 1993, isbn 0-444-89880-8

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: 129-156

Michael J. C. Gordon: Introduction to the HOL System. TPHOLs 1991: 2-3

Michael J. C. Gordon: Programming language theory and its implementation - applicative and imperative paradigms. Prentice Hall International series in Computer Science, Prentice Hall 1988, isbn 978-0-13-730409-7, pp. I-XIV, 1-255

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

Michael J. C. Gordon: The Denotational Semantics of Sequential Machines. Inf. Process. Lett. 10(1): 1-3 (1980)

Michael J. C. Gordon: The denotational description of programming languages - an introduction. Springer 1979, isbn 978-3-540-90433-5, pp. 1-160

Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth: Edinburgh LCF. Lecture Notes in Computer Science 78, Springer 1979, isbn 3-540-09724-4

Michael J. C. Gordon: On the Power of List Iteration. Comput. J. 22(4): 376-379 (1979)

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