Michael J. C. Gordon

According to our database, Michael J. C. Gordon authored at least 45 papers between 1974 and 2012.

Collaborative distances:

• Dijkstra number of two.
• Erdős number of three.

2012

Function extraction.

Magnus O. Myreen, Michael J. C. Gordon

Sci. Comput. Program., 2012

Decompilation into logic - Improved.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011

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

2010

ML: metalanguage or object language?

Michael J. C. Gordon

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Specification and Verification of ARM Hardware and Software.

Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

Forward with Hoare.

Mike Gordon, Hélène Collavizza

Proceedings of the Reflections on the Work of C. A. R. Hoare., 2010

2009

Verified LISP Implementations on ARM, x86 and PowerPC.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Extensible Proof-Producing Compilation.

Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon

Proceedings of the Compiler Construction, 18th International Conference, 2009

2008

Transforming Programs into Recursive Functions.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 2008

Twenty Years of Theorem Proving for HOLs Past, Present and Future.

Mike Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

Proof producing synthesis of arithmetic and cryptographic hardware.

Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon

Formal Aspects Comput., 2007

Hoare Logic for Realistically Modelled Machine Code.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Hoare Logic for ARM Machine Code.

Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon

Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

2006

Model Checking PSL Using HOL and SMV.

Thomas Tuerk, Klaus Schneider, Mike Gordon

Proceedings of the Hardware and Software, 2006

An Integration of HOL and ACL2.

Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

An embedding of the ACL2 logic in HOL.

Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2005

Automatic Formal Synthesis of Hardware from Higher Order Logic.

Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind

Proceedings of the 5th International Workshop on Automated Verification of Critical Systems, 2005

2003

Validating the PSL/Sugar Semantics Using Automated Reasoning.

Michael J. C. Gordon

Formal Aspects Comput., 2003

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.

Michael J. C. Gordon, Joe Hurd, Konrad Slind

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

Programming Combinations of Deduction and BDD-based Symbolic Calculation.

Michael J. C. Gordon

LMS J. Comput. Math., 2002

Relating Event and Trace Semantics of Hardware Description Languages.

Michael J. C. Gordon

Comput. J., 2002

PuzzleTool : An Example of Programming Computation and Deduction.

Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2000

Christopher Strachey: Recollections of His Influence.

Michael J. C. Gordon

High. Order Symb. Comput., 2000

Reachability Programming in HOL98 Using BDDs.

Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 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

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

From LCF to HOL: a short history.

Mike Gordon

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1998

An Interface between Clam and HOL.

Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

System Description: An Interface Between CL^AM and HOL.

Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy

Proceedings of the Automated Deduction, 1998

1996

Set Theory, Higher Order Logic or Both?

Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

1995

A shallow embedding of Z in HOL.

Jonathan P. Bowen, Mike Gordon

Inf. Softw. Technol., 1995

Experiments with ZF Set Theory in HOL and Isabelle.

Sten Agerholm, Michael J. C. Gordon

Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1995

The Semantic Challenge of Verilog HDL

Michael J. C. Gordon

Proceedings of the Proceedings, 1995

1994

Z and HOL.

Jonathan P. Bowen, Michael J. C. Gordon

Proceedings of the Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings, 1994

1993

A Verifier and Timing Analyser for Simple Imperative Programs (Abstract).

Michael J. C. Gordon

Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992

Experience with Embedding Hardware Description Languages in HOL.

Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel

Proceedings of the Theorem Provers in Circuit Design, 1992

1991

Introduction to the HOL System.

Michael J. C. Gordon

Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991

1988

Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic

C. A. R. Hoare, Michael J. C. Gordon

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

Programming language theory and its implementation - applicative and imperative paradigms.

Michael J. C. Gordon

Prentice Hall International series in Computer Science, Prentice Hall, ISBN: 978-0-13-730409-7, 1988

1980

The Denotational Semantics of Sequential Machines.

Michael J. C. Gordon

Inf. Process. Lett., 1980

1979

On the Power of List Iteration.

Michael J. C. Gordon

Comput. J., 1979

Edinburgh LCF

Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth

Lecture Notes in Computer Science 78, Springer, ISBN: 3-540-09724-4, 1979

The denotational description of programming languages - an introduction.

Michael J. C. Gordon

Springer, ISBN: 978-3-540-90433-5, 1979

1978

A Metalanguage for Interactive Proof in LCF.

Michael J. C. Gordon, Robin Milner, F. Lockwood Morris, Malcolm C. Newey, Christopher P. Wadsworth

Proceedings of the Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, 1978

1974

Evaluation and denotation of pure LISP programs : a worked example in semantics.

Michael J. C. Gordon

PhD thesis, 1974