The following pages link to Michael J. C. Gordon (Q436371):
Displaying 16 items.
- Function extraction (Q436372) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- Validating the PSL/Sugar semantics using automated reasoning (Q706502) (← links)
- The denotational semantics of sequential machines (Q1133896) (← links)
- (Q1801220) (redirect page) (← links)
- Edinburgh LCF. A mechanized logic of computation (Q1801222) (← links)
- (Q2754043) (← links)
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’ (Q2955752) (← links)
- Hoare Logic for ARM Machine Code (Q3508532) (← links)
- On the power of list iteration (Q3860813) (← links)
- (Q4199490) (← links)
- Relating Event and Trace Semantics of Hardware Description Languages (Q4328965) (← links)
- (Q4484342) (← links)
- Programming Combinations of Deduction and BDD-based Symbolic Calculation (Q4827596) (← links)
- Transforming Programs into Recursive Functions (Q5179363) (← links)
- Hoare Logic for Realistically Modelled Machine Code (Q5758130) (← links)
