Michael J. C. Gordon - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 37 from 37

2012

Function extractionMagnus O. Myreen, Michael J. C. Gordon. SCP, 77(4):505-517, 2012. [doi]

Decompilation into logic - ImprovedMagnus O. Myreen, Michael J. C. Gordon, Konrad Slind. FMCAD 2012: 78-81 [doi]

2011

The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4Michael J. C. Gordon, Matt Kaufmann, Sandip Ray. JAR, 47(1):1-16, 2011. [doi]

2010

Specification and Verification of ARM Hardware and SoftwareAnthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications. pages 221-247, Springer, 2010. [doi]

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

2009

Verified LISP Implementations on ARM, x86 and PowerPCMagnus O. Myreen, Michael J. C. Gordon. tphol 2009: 359-374 [doi]

Transforming Programs into Recursive FunctionsMagnus O. Myreen, Michael J. C. Gordon. ENTCS, 240:185-200, 2009. [doi]

Extensible Proof-Producing CompilationMagnus O. Myreen, Konrad Slind, Michael J. C. Gordon. CC 2009: 2-16 [doi]

2008

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

2007

Hoare Logic for ARM Machine CodeMagnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon. fsen 2007: 272-286 [doi]

Hoare Logic for Realistically Modelled Machine CodeMagnus O. Myreen, Michael J. C. Gordon. TACAS 2007: 568-582 [doi]

2006

An embedding of the ACL2 logic in HOLMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds. acl2 2006: 40-46 [doi]

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

2003

Validating the PSL/Sugar Semantics Using Automated ReasoningMichael J. C. Gordon. fac, 15(4):406-421, 2003. [doi]

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem ProvingMichael J. C. Gordon, Joe Hurd, Konrad Slind. charme 2003: 200-215 [doi]

2002

Relating Event and Trace Semantics of Hardware Description LanguagesMichael J. C. Gordon. cj, 45(1):27-36, 2002. [doi]

PuzzleTool : An Example of Programming Computation and DeductionMichael J. C. Gordon. tphol 2002: 214-229 [doi]

2000

The PROSPER ToolkitLouise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham. TACAS 2000: 78-92 [doi]

Christopher Strachey: Recollections of His InfluenceMichael J. C. Gordon. lisp, 13(1/2):65-67, 2000.

Reachability Programming in HOL98 Using BDDsMichael J. C. Gordon. tphol 2000: 179-196

1998

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

System Description: An Interface Between CL:::A:::M and HOLKonrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy. cade 1998: 134-138 [doi]

1996

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

1995

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

The Semantic Challenge of Verilog HDLMichael J. C. Gordon. lics 1995: 136-145

1994

Z and HOLJonathan P. Bowen, Michael J. C. Gordon. zum 1994: 141-167

1993

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

1992

Experience with Embedding Hardware Description Languages in HOLRichard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel. tpcd 1992: 129-156

1991

Introduction to the HOL SystemMichael J. C. Gordon. tphol 1992: 2-3

1988

Programming language theory and its implementation - applicative and imperative paradigmsMichael J. C. Gordon. Prentice Hall International series in Computer Science, Prentice Hall, 1988.

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

1980

The Denotational Semantics of Sequential MachinesMichael J. C. Gordon. ipl, 10(1):1-3, 1980.

1979

The denotational description of programming languages - an introductionMichael J. C. Gordon. Springer, 1979.

On the Power of List IterationMichael J. C. Gordon. cj, 22(4):376-379, 1979.

Edinburgh LCFMichael J. C. Gordon, Robin Milner, Christopher P. Wadsworth. Volume 78 of Lecture Notes in Computer Science, Springer, 1979.

1978

A Metalanguage for Interactive Proof in LCFMichael J. C. Gordon, Robin Milner, L. Morris, Malcolm C. Newey, Christopher P. Wadsworth. POPL 1978: 119-130

1974

Evaluation and denotation of pure LISP programs : a worked example in semanticsMichael J. C. Gordon. PhD thesis, University of Edinburgh, UK, 1974. [doi]

Sign in or sign up to see more results.

runs on WebDSL