Michael J. C. Gordon

39 papers A* 4A 4B 4Journal 8Unranked 13

Year	Rank	Type	Title / Venue / Authors
2012	B	`conf`	Decompilation into logic - Improved. FMCAD Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
2012	J	`jnl`	Function extraction. Sci. Comput. Program. Magnus O. Myreen, Michael J. C. Gordon
2011	J	`jnl`	The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. J. Autom. Reason. Michael J. C. Gordon, Matt Kaufmann, Sandip Ray
2010	A	`conf`	ML: metalanguage or object language? ICFP Michael J. C. Gordon
2010	—	`ch.`	Specification and Verification of ARM Hardware and Software. Design and Verification of Microprocessor Systems for High-Assurance Applications Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen
2009	B	`conf`	Extensible Proof-Producing Compilation. CC Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
2009	—	`conf`	Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs Magnus O. Myreen, Michael J. C. Gordon
2008	B	`conf`	Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
2008	—	`conf`	Transforming Programs into Recursive Functions. SBMF Magnus O. Myreen, Michael J. C. Gordon
2007	—	`conf`	Hoare Logic for ARM Machine Code. FSEN Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
2007	A	`conf`	Hoare Logic for Realistically Modelled Machine Code. TACAS Magnus O. Myreen, Michael J. C. Gordon
2006	B	`conf`	An Integration of HOL and ACL2. FMCAD Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
2006	—	`conf`	An embedding of the ACL2 logic in HOL. ACL2 Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
2003	—	`conf`	Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. CHARME Michael J. C. Gordon, Joe Hurd, Konrad Slind
2003	J	`jnl`	Validating the PSL/Sugar Semantics Using Automated Reasoning. Formal Aspects Comput. Michael J. C. Gordon
2002	J	`jnl`	Programming Combinations of Deduction and BDD-based Symbolic Calculation. LMS J. Comput. Math. Michael J. C. Gordon
2002	—	`conf`	PuzzleTool : An Example of Programming Computation and Deduction. TPHOLs Michael J. C. Gordon
2002	J	`jnl`	Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. Michael J. C. Gordon
2000	J	`jnl`	Christopher Strachey: Recollections of His Influence. High. Order Symb. Comput. Michael J. C. Gordon
2000	—	`conf`	Reachability Programming in HOL98 Using BDDs. TPHOLs Michael J. C. Gordon
2000	A	`conf`	The PROSPER Toolkit. TACAS Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
1998	—	`conf`	An Interface between Clam and HOL. TPHOLs Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon
1998	A	`conf`	System Description: An Interface Between CL CADE Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy
1996	—	`conf`	Set Theory, Higher Order Logic or Both? TPHOLs Michael J. C. Gordon
1995	—	`conf`	Experiments with ZF Set Theory in HOL and Isabelle. TPHOLs Sten Agerholm, Michael J. C. Gordon
1995	A*	`conf`	The Semantic Challenge of Verilog HDL LICS Michael J. C. Gordon
1994	—	`conf`	Z and HOL. Z User Workshop Jonathan P. Bowen, Michael J. C. Gordon
1993	A*	`conf`	A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). CAV Michael J. C. Gordon
1993	—	`ed.`	Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992 TPHOLs Luc J. M. Claesen, Michael J. C. Gordon
1992	—	`conf`	Experience with Embedding Hardware Description Languages in HOL. TPCD Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel
1991	—	`conf`	Introduction to the HOL System. TPHOLs Michael J. C. Gordon
1988	A*	`conf`	Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic LICS C. A. R. Hoare, Michael J. C. Gordon
1988	—	`book`	Programming language theory and its implementation - applicative and imperative paradigms. Michael J. C. Gordon
1980	J	`jnl`	The Denotational Semantics of Sequential Machines. Inf. Process. Lett. Michael J. C. Gordon
1979	—	`book`	Edinburgh LCF Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth
1979	J	`jnl`	On the Power of List Iteration. Comput. J. Michael J. C. Gordon
1979	—	`book`	The denotational description of programming languages - an introduction. Michael J. C. Gordon
1978	A*	`conf`	A Metalanguage for Interactive Proof in LCF. POPL Michael J. C. Gordon, Robin Milner, F. Lockwood Morris, Malcolm C. Newey, Christopher P. Wadsworth
1974	—	`—`	Evaluation and denotation of pure LISP programs : a worked example in semantics. Michael J. C. Gordon