The following is a list of possible projects that can be done as part of the evaluation of the graduate course at the University of Pisa taught by Miller in April 2014 titled "The proof theoretic foundation of computational logic". The class notes and handouts are likely to be useful for these projects. Additional references are suggested. Others can be used as needed. In all cases, the result of these projects are reports that should illustrate your understanding, both technical and high-level, of the topics proposed.
Project 1: Comment on the general relationship between logic programming and the sequent calculus. When Gentzen introduced the sequent calculus, he was trying to get certain results (eg, cut-elimination) for classical and intuitionistic logic. Years later, the sequent calculus has been used to describe something much smaller than all of logic: namely, logic programming. Discuss the general relationship between logic programming and sequent calculus from what you can find in the following three papers: [MNPS], [JNS], [LM]. The lecture notes would also be helpful here.
Project 2: Read the paper [HM] on the linear logic language Lolli and implement an interpreter for Lolli in Prolog or (better) λProlog. Develop several examples of programs in Lolli. Notice that there is an interpreter for Lolli in Prolog available in the reference below. Feel free to us it and improve it. Experiment with new examples of linear logic programming (not just those available in the link below). Write a report describing the high-level aspects of your implementation and your experience with your example linear logic programs.
Project 3: Discuss the possible relationship between model checking (using, say LTL) and classical logic with fixed points (accompanied by the rule for unfolding fixed points: that is, there is no induction and co-induction rules). Most traditional approaches to model checking are not described in proof theoretic terms. Take some standard, simple model checking problems and show how they can be expressed in the sequent calculus with inference rules for fixed point unfolding (and equality). For a background in model checking, read [Emerson]. For the proof theory of fixed points and equality, read the papers [Baelde], [BM], and [BGMNT].