Comments on the thesis work of Raymond McDowell
McDowell completed his PhD titled ``Reasoning in a Logic with
Definitions and Induction'' in September 1997. His thesis is
available in DVI and PDF formats.
Since the completion of his PhD, McDowell has published three papers
with co-authors related to his thesis.
-
Raymond McDowell and Dale Miller.
Cut-Elimination for a Logic with Definitions and Induction,
Theoretical Computer Science, volume 232, pages 91 - 119 (2000).
(DVI,
PostScript,
PDF). Some comments and errata.
-
Raymond McDowell and Dale Miller.
Reasoning with Higher-Order Abstract Syntax in a Logical
Framework, ACM Transactions
on Computational Logic Volume 3, Number 1 (January 2002), 80 - 136 (PDF).
-
Raymond McDowell, Dale Miller, and Catuscia Palamidessi.
Encoding Transition Systems in Sequent Calculus,
Theoretical Computer Science, 294(3), 411-437 (2003).
(DVI,
PostScript,
PDF).
A preliminary report appears in
the Proceedings of the 1996 Workshop on Linear Logic and is available in
Volume 3 of
ENTCS
(DVI,
PostScript,
PDF).
Many of the examples in the ToCL 2002 paper above make use of a
technical device called "explicit eigenvariable encoding". While this
technique works to establish a number of formal proof, it was a rather
heavy and painful encoding. In subsequent work, Miller and Alwen Tiu
have found a more declarative approach to this kind of encoding. Their
solution (LICS03: PDF, PS, DVI) involved a new logical
quantifier called nabla.