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.

  1. 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.
  2. 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).
  3. 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.