Travelled to:1 × Greece
1 × Portugal
2 × Germany
2 × United Kingdom
3 × USA
Collaborated with:∅ M.O.Myreen K.Slind C.A.R.Hoare R.J.Boulton A.Bundy R.Milner L.Morris M.C.Newey C.P.Wadsworth L.A.Dennis G.Collins M.Norrish G.Robinson T.F.Melham
Talks about:metalanguag (2) proof (2) logic (2) interfac (1) interact (1) descript (1) challeng (1) verilog (1) toolkit (1) realist (1)
Person: Michael J. C. Gordon
DBLP: Gordon:Michael_J=_C=
Contributed to:
2010
2009
20072000
1998
1995
19931988
1978Wrote 9 papers:
- ICFP-2010-Gordon #metalanguage #ml #named #question
- ML: metalanguage or object language? (MJCG), pp. 1–2.
- CC-2009-MyreenSG #compilation
- Extensible Proof-Producing Compilation (MOM, KS, MJCG), pp. 2–16.
- TACAS-2007-MyreenG #hoare #logic
- Hoare Logic for Realistically Modelled Machine Code (MOM, MJCG), pp. 568–582.
- TACAS-2000-DennisCNBSRGM #tool support
- The PROSPER Toolkit (LAD, GC, MN, RJB, KS, GR, MJCG, TFM), pp. 78–92.
- CADE-1998-SlindGBB #interface
- System Description: An Interface Between CLAM and HOL (KS, MJCG, RJB, AB), pp. 134–138.
- LICS-1995-Gordon #challenge #semantics
- The Semantic Challenge of Verilog HDL (MJCG), pp. 136–145.
- CAV-1993-Gordon #imperative #source code #verification
- A Verifier and Timing Analyser for Simple Imperative Programs (MJCG), p. 320.
- LICS-1988-HoareG #correctness #logic
- Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic (CARH, MJCG), pp. 28–36.
- POPL-1978-GordonMMNW #interactive #metalanguage #proving
- A Metalanguage for Interactive Proof in LCF (MJCG, RM, LM, MCN, CPW), pp. 119–130.