Michael J. C. Gordon

	2012
35		Magnus O. Myreen, Michael J. C. Gordon: Function extraction. Sci. Comput. Program. 77(4): 505-517 (2012)
	2011
34		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)
	2010
33		Michael J. C. Gordon: ML: metalanguage or object language? ICFP 2010: 1-2
	2009
32		Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon: Extensible Proof-Producing Compilation. CC 2009: 2-16
31		Magnus O. Myreen, Michael J. C. Gordon: Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs 2009: 359-374
30		Magnus O. Myreen, Michael J. C. Gordon: Transforming Programs into Recursive Functions. Electr. Notes Theor. Comput. Sci. 240: 185-200 (2009)
	2008
29		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
	2007
28		Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon: Hoare Logic for ARM Machine Code. FSEN 2007: 272-286
27		Magnus O. Myreen, Michael J. C. Gordon: Hoare Logic for Realistically Modelled Machine Code. TACAS 2007: 568-582
	2006
26		Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
25		Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
	2003
24		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
23		Michael J. C. Gordon: Validating the PSL/Sugar Semantics Using Automated Reasoning. Formal Asp. Comput. 15(4): 406-421 (2003)
	2002
22		Michael J. C. Gordon: PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs 2002: 214-229
21		Michael J. C. Gordon: Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45(1): 27-36 (2002)
	2000
20		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
19		Michael J. C. Gordon: Reachability Programming in HOL98 Using BDDs. TPHOLs 2000: 179-196
18		Michael J. C. Gordon: Christopher Strachey: Recollections of His Influence. Higher-Order and Symbolic Computation 13(1/2): 65-67 (2000)
	1998
17		Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy: System Description: An Interface Between CLAM and HOL. CADE 1998: 134-138
16		Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon: An Interface between Clam and HOL. TPHOLs 1998: 87-104
	1996
15		Michael J. C. Gordon: Set Theory, Higher Order Logic or Both? TPHOLs 1996: 191-201
	1995
14		Michael J. C. Gordon: The Semantic Challenge of Verilog HDL LICS 1995: 136-145
13		Sten Agerholm, Michael J. C. Gordon: Experiments with ZF Set Theory in HOL and Isabelle. TPHOLs 1995: 32-45
	1994
12		Jonathan P. Bowen, Michael J. C. Gordon: Z and HOL. Z User Workshop 1994: 141-167
	1993
11		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
10		Michael J. C. Gordon: A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). CAV 1993: 320
	1992
9		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
	1991
8		Michael J. C. Gordon: Introduction to the HOL System. TPHOLs 1991: 2-3
	1988
7		Michael J. C. Gordon: Programming language theory and its implementation - applicative and imperative paradigms. Prentice Hall 1988: I-XIV, 1-255
6		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
5		Michael J. C. Gordon: The Denotational Semantics of Sequential Machines. Inf. Process. Lett. 10(1): 1-3 (1980)
	1979
4		Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth: Edinburgh LCF Springer 1979
3		Michael J. C. Gordon: The denotational description of programming languages - an introduction. Springer 1979: 1-160
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

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

Colors in the list of coauthors

Last update Wed May 30 22:34:44 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page