dblp.uni-trier.dewww.uni-trier.de

Michael J. C. Gordon Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
30EEMagnus O. Myreen, Konrad Slind, Michael J. C. Gordon: Extensible Proof-Producing Compilation. CC 2009: 2-16
29EEMagnus O. Myreen, Michael J. C. Gordon: Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs 2009: 359-374
28EEMagnus O. Myreen, Michael J. C. Gordon: Transforming Programs into Recursive Functions. Electr. Notes Theor. Comput. Sci. 240: 185-200 (2009)
2008
27EEMagnus O. Myreen, Michael J. C. Gordon, Konrad Slind: Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD 2008: 1-8
2007
26EEMagnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon: Hoare Logic for ARM Machine Code. FSEN 2007: 272-286
25EEMagnus O. Myreen, Michael J. C. Gordon: Hoare Logic for Realistically Modelled Machine Code. TACAS 2007: 568-582
2006
24EEMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
23EEMichael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
2003
22EEMichael 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
21EEMichael J. C. Gordon: Validating the PSL/Sugar Semantics Using Automated Reasoning. Formal Asp. Comput. 15(4): 406-421 (2003)
2002
20EEMichael J. C. Gordon: PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs 2002: 214-229
19EEMichael J. C. Gordon: Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45(1): 27-36 (2002)
2000
18EELouise 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
17EEMichael J. C. Gordon: Reachability Programming in HOL98 Using BDDs. TPHOLs 2000: 179-196
16 Michael J. C. Gordon: Christopher Strachey: Recollections of His Influence. Higher-Order and Symbolic Computation 13(1/2): 65-67 (2000)
1998
15EEKonrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy: System Description: An Interface Between CLAM and HOL. CADE 1998: 134-138
14EERichard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon: An Interface between Clam and HOL. TPHOLs 1998: 87-104
1996
13EEMichael J. C. Gordon: Set Theory, Higher Order Logic or Both? TPHOLs 1996: 191-201
1995
12 Michael J. C. Gordon: The Semantic Challenge of Verilog HDL LICS 1995: 136-145
11EESten Agerholm, Michael J. C. Gordon: Experiments with ZF Set Theory in HOL and Isabelle. TPHOLs 1995: 32-45
1994
10 Jonathan P. Bowen, Michael J. C. Gordon: Z and HOL. Z User Workshop 1994: 141-167
1993
9 Luc J. M. Claesen, Michael J. C. Gordon: Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992 North-Holland/Elsevier 1993
8EEMichael J. C. Gordon: A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). CAV 1993: 320
1992
7 Richard J. Boulton, Andrew Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel: Experience with Embedding Hardware Description Languages in HOL. TPCD 1992: 129-156
1991
6 Michael J. C. Gordon: Introduction to the HOL System. TPHOLs 1991: 2-3
1988
5 C. A. R. Hoare, Michael J. C. Gordon: Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic LICS 1988: 28-36
1980
4 Michael J. C. Gordon: The Denotational Semantics of Sequential Machines. Inf. Process. Lett. 10(1): 1-3 (1980)
1979
3 Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth: Edinburgh LCF Springer 1979
2 Michael J. C. Gordon: On the Power of List Iteration. Comput. J. 22(4): 376-379 (1979)
1978
1 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

Coauthor Index

1Sten Agerholm [11]
2Richard J. Boulton [7] [14] [15] [18]
3Jonathan P. Bowen [10]
4Alan Bundy [14] [15]
5Luc J. M. Claesen [9]
6Graham Collins [18]
7Louise A. Dennis [18]
8Anthony C. J. Fox [26]
9Andrew Gordon [7]
10John Harrison [7]
11John Herbert [7]
12C. A. R. Hoare (Tony Hoare) [5]
13Warren A. Hunt Jr. [23] [24]
14Joe Hurd [22]
15Matt Kaufmann [23] [24]
16Thomas F. Melham [18]
17Robin Milner [1] [3]
18L. Morris [1]
19Magnus O. Myreen [25] [26] [27] [28] [29] [30]
20Malcolm C. Newey [1]
21Michael Norrish [18]
22James Reynolds [23] [24]
23Graham Robinson [18]
24Konrad Slind [14] [15] [18] [22] [27] [30]
25John Van Tassel [7]
26Christopher P. Wadsworth [1] [3]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)