Michael J. C. Gordon

Available identifiers

Publication	Date of Publication	Type
Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’	2017-01-13	Paper
Transforming Programs into Recursive Functions	2015-03-19	Paper
Function extraction	2012-07-20	Paper
The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4	2011-06-03	Paper
Hoare Logic for ARM Machine Code	2008-07-01	Paper
Hoare Logic for Realistically Modelled Machine Code	2007-09-03	Paper
Validating the PSL/Sugar semantics using automated reasoning	2005-02-08	Paper
Programming Combinations of Deduction and BDD-based Symbolic Calculation	2004-11-18	Paper
https://portal.mardi4nfdi.de/entity/Q4484342	2003-06-12	Paper
Relating Event and Trace Semantics of Hardware Description Languages	2003-04-06	Paper
https://portal.mardi4nfdi.de/entity/Q2754043	2001-11-11	Paper
Edinburgh LCF. A mechanized logic of computation	1993-06-05	Paper
The denotational semantics of sequential machines	1980-01-01	Paper
https://portal.mardi4nfdi.de/entity/Q4199490	1979-01-01	Paper
On the power of list iteration	1979-01-01	Paper

This page was built for person: Michael J. C. Gordon