The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Michael J. C. Gordon: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Michael J. C. Gordon, Robin Milner, L. Morris, Malcolm C. Newey, Christopher P. Wadsworth
    A Metalanguage for Interactive Proof in LCF. [Citation Graph (3, 0)][DBLP]
    POPL, 1978, pp:119-130 [Conf]
  2. Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy
    System Description: An Interface Between CLAM and HOL. [Citation Graph (0, 0)][DBLP]
    CADE, 1998, pp:134-138 [Conf]
  3. Michael J. C. Gordon
    A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). [Citation Graph (0, 0)][DBLP]
    CAV, 1993, pp:320- [Conf]
  4. Michael J. C. Gordon, Joe Hurd, Konrad Slind
    Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. [Citation Graph (0, 0)][DBLP]
    CHARME, 2003, pp:200-215 [Conf]
  5. Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
    An Integration of HOL and ACL2. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2006, pp:153-160 [Conf]
  6. Michael J. C. Gordon
    The Semantic Challenge of Verilog HDL [Citation Graph (0, 0)][DBLP]
    LICS, 1995, pp:136-145 [Conf]
  7. C. A. R. Hoare, Michael J. C. Gordon
    Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic [Citation Graph (0, 0)][DBLP]
    LICS, 1988, pp:28-36 [Conf]
  8. Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
    The PROSPER Toolkit. [Citation Graph (0, 0)][DBLP]
    TACAS, 2000, pp:78-92 [Conf]
  9. Richard J. Boulton, Andrew Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel
    Experience with Embedding Hardware Description Languages in HOL. [Citation Graph (0, 0)][DBLP]
    TPCD, 1992, pp:129-156 [Conf]
  10. Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon
    An Interface between Clam and HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1998, pp:87-104 [Conf]
  11. Sten Agerholm, Michael J. C. Gordon
    Experiments with ZF Set Theory in HOL and Isabelle. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1995, pp:32-45 [Conf]
  12. Michael J. C. Gordon
    Reachability Programming in HOL98 Using BDDs. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:179-196 [Conf]
  13. Michael J. C. Gordon
    PuzzleTool : An Example of Programming Computation and Deduction. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2002, pp:214-229 [Conf]
  14. Michael J. C. Gordon
    Introduction to the HOL System. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1991, pp:2-3 [Conf]
  15. Michael J. C. Gordon
    Set Theory, Higher Order Logic or Both? [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1996, pp:191-201 [Conf]
  16. Jonathan P. Bowen, Michael J. C. Gordon
    Z and HOL. [Citation Graph (0, 0)][DBLP]
    Z User Workshop, 1994, pp:141-167 [Conf]
  17. Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
    An embedding of the ACL2 logic in HOL. [Citation Graph (0, 0)][DBLP]
    ACL2, 2006, pp:40-46 [Conf]
  18. Michael J. C. Gordon
    Relating Event and Trace Semantics of Hardware Description Languages. [Citation Graph (0, 0)][DBLP]
    Comput. J., 2002, v:45, n:1, pp:27-36 [Journal]
  19. Michael J. C. Gordon
    On the Power of List Iteration. [Citation Graph (0, 0)][DBLP]
    Comput. J., 1979, v:22, n:4, pp:376-379 [Journal]
  20. Michael J. C. Gordon
    Validating the PSL/Sugar Semantics Using Automated Reasoning. [Citation Graph (0, 0)][DBLP]
    Formal Asp. Comput., 2003, v:15, n:4, pp:406-421 [Journal]
  21. Michael J. C. Gordon
    The Denotational Semantics of Sequential Machines. [Citation Graph (0, 0)][DBLP]
    Inf. Process. Lett., 1980, v:10, n:1, pp:1-3 [Journal]
  22. Michael J. C. Gordon
    Christopher Strachey: Recollections of His Influence. [Citation Graph (0, 0)][DBLP]
    Higher-Order and Symbolic Computation, 2000, v:13, n:1/2, pp:65-67 [Journal]
  23. Magnus O. Myreen, Michael J. C. Gordon
    Hoare Logic for Realistically Modelled Machine Code. [Citation Graph (0, 0)][DBLP]
    TACAS, 2007, pp:568-582 [Conf]
  24. Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
    Hoare Logic for ARM Machine Code. [Citation Graph (0, 0)][DBLP]
    FSEN, 2007, pp:272-286 [Conf]

  25. Extensible Proof-Producing Compilation. [Citation Graph (, )][DBLP]


  26. Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. [Citation Graph (, )][DBLP]


  27. Verified LISP Implementations on ARM, x86 and PowerPC. [Citation Graph (, )][DBLP]


  28. Transforming Programs into Recursive Functions. [Citation Graph (, )][DBLP]


Search in 0.036secs, Finished in 0.037secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002