BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Gordon:Michael_J=_C=

Contributed to:

ICFP 20102010
CC 20092009
TACAS 20072007
TACAS 20002000
CADE 19981998
LICS 19951995
CAV 19931993
LICS 19881988
POPL 19781978

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.