Relational specifications are commonly used in computer science to describe a range of computationally important topics. Such specifications generally involve collections of predicates and inference rules (or, equivalently, logic clauses, or inductive definitions) involving those predicates. For examples, logic programs are examples of relational specifications. Structured operational semantics definitions of a programming languages evaluation and typing are also examples of relational specifications. As a result, a great deal of the meta-theory about programming languages and specification languages (such as the λ-calculus and π-calculus) can be seen as proving properties of logic specifications.
Miller and his colleagues and students have been developing approaches to reasoning about relational specifications in recent years (see [1,2,3] below). Most of that work has been foundational: new proof theoretic ideas and results have been established that should make it more tractable to automate a wide range of theorems about relational specifications. This training project will focus on trying to exploit some of that recent work in order to prove a range of simple properties about relational specifications.
One specific goal is to apply this recent work on proof theory to the design of automatic procedures that could prove the following simple theorems. Once such theorems have been proved, proofs of such theorems must also be described.
Once this class of examples has been addressed, other examples, such as those in the POPLmark challenge [4] or those related to the Twelf theorem prover [5] could be attempted.
Given the duration of this stage, the main focus is on design of automated procedures and not their efficient implementation. The team does have some software tools (in particular, Bedwyr, Taci [6,7]) that can help in developing some prototypes for exploring large examples.
PhD thesis topics are possible based on work done for this stage.
Least and greatest fixed points in linear logic by David Baelde and Dale Miller. LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning (PDF).
Focusing and Polarization in Intuitionistic Logic by Chuck Liang and Dale Miller. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 451-465. Springer-Verlag. (PDF). Slides used at the conference. Extended version of paper dated 15 Dec 2006. HAL.
A Proof Theory for Generic Judgments, by Dale Miller and Alwen Tiu. ACM Transactions on Computational Logic, 6(4), pp. 749--783, October 2005. (dvi, ps, pdf).
Mechanized Metatheory for the Masses: The PoplMark Challenge by Aydemir, Bohannon, Fairbairn, Foster, Pierce, Sewell, Vytiniotis, Washburn, Weirich, and Zdancewic, in Theorem Proving in Higher Order Logics: 18th International Conference, 2005, LNCS 3603, pp. 50--65. See the wiki for the POPLmark Challenge languages.
A coverage checking algorithm for LF, Carsten Schürmann and Frank Pfenning. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), pages 120-135, Rome, Italy, September 2003. Springer-Verlag LNCS 2758. [PDF] [PS]
The Bedwyr system for model checking over syntactic expressions by David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. CADE 2007: 21th Conference on Automated Deduction, Frank Pfenning, editor, LNAI 4603, pages 391-397. Springer, 2007. (pdf)
The model checking system Bedwyr and the interactive theorem prover Taci are available as open source software. Taci is not officially supported and is mostly used internally to the Parsifal team.