Tools and Techniques for Verification of System Infrastructure was held in honour of Prof. Michael J. C. Gordon FRS, on the occasion of his 60th birthday.
Abstract Proceedings
A proceedings was distributed at the meeting containing abstracts from the invited speakers and poster authors. This is available for download in PDF format (0.5Mb).
Journal Special Issue
A selection of papers that followed from the meeting were published in a special issue of the Journal of Automated Reasoning, entitled Computer Assisted Reasoning: A Festschrift for Michael J. C. Gordon and guest edited by Richard Boulton, Joe Hurd and Konrad Slind. Here is the bibliographic data for the papers published in the special issue:
@article{boulton2009,
author = {Richard Boulton and Joe Hurd and Konrad Slind},
title = {Computer Assisted Reasoning: A {F}estschrift for {M}ichael {J.} {C.} {G}ordon},
journal = {Special Issue of the Journal of Automated Reasoning},
month = oct,
year = 2009,
volume = 43,
number = 3,
pages = {237--242},
url = {http://www.springerlink.com/content/5650666043651557/}
}
@article{harrison2009,
author = {John Harrison},
title = {Formalizing an Analytic Proof of the Prime Number Theorem},
journal = {Special Issue of the Journal of Automated Reasoning},
month = oct,
year = 2009,
volume = 43,
number = 3,
pages = {243--261},
url = {http://www.springerlink.com/content/x35225442882h618/},
abstract =
{We describe the computer formalization of a
complex-analytic proof of the Prime Number Theorem (PNT), a classic
result from number theory characterizing the asymptotic density of the
primes. The formalization, conducted using the HOL Light theorem
prover, proceeds from the most basic axioms for mathematics yet builds
from that foundation to develop the necessary analytic machinery
including Cauchy’s integral formula, so that we are able to formalize
a direct, modern and elegant proof instead of the more involved
`elementary' Erdös-Selberg argument. As well as setting the work in
context and describing the highlights of the formalization, we analyze
the relationship between the formal proof and its informal counterpart
and so attempt to derive some general lessons about the formalization
of mathematics.}
}
@article{blazy2009,
author = {Sandrine Blazy and Xavier Leroy},
title = {Mechanized Semantics for the {C}light Subset of the {C} Language},
journal = {Special Issue of the Journal of Automated Reasoning},
month = oct,
year = 2009,
volume = 43,
number = 3,
pages = {263--288},
url = {http://www.springerlink.com/content/l2422j427262l3h6/},
abstract =
{This article presents the formal semantics of a
large subset of the C language called Clight. Clight includes pointer
arithmetic, struct and union types, C loops and structured switch
statements. Clight is the source language of the CompCert verified
compiler. The formal semantics of Clight is a big-step operational
semantics that observes both terminating and diverging executions and
produces traces of input/output events. The formal semantics of Clight
is mechanized using the Coq proof assistant. In addition to the
semantics of Clight, this article describes its integration in the
CompCert verified compiler and several ways by which the semantics was
validated.}
}
@article{nipkow2009,
author = {Tobias Nipkow},
title = {Social Choice Theory in {HOL}},
journal = {Special Issue of the Journal of Automated Reasoning},
month = oct,
year = 2009,
volume = 43,
number = 3,
pages = {289--304},
url = {http://www.springerlink.com/content/gj8qx75506626830/},
abstract =
{This article presents formalizations in
higher-order logic of two proofs of Arrow’s impossibility theorem due
to Geanakoplos. The Gibbard-Satterthwaite theorem is derived as a
corollary. Lacunae found in the literature are discussed.}
}
@article{norrish2009,
author = {Michael Norrish},
title = {Rewriting Conversions Implemented with Continuations},
journal = {Special Issue of the Journal of Automated Reasoning},
month = oct,
year = 2009,
volume = 43,
number = 3,
pages = {305--336},
url = {http://www.springerlink.com/content/903vr1g4rn114816/},
abstract =
{We give a continuation-based implementation of
rewriting for systems in the LCF tradition. These systems must
construct explicit proofs of equations when rewriting, and currently
do so in a way that can be very space-inefficient. An explicit
representation of continuations improves performance on large terms,
and on long-running computations.}
}