INRIA EA RAPT Report 2011

Exchanges

Internships

• Andrew Cave (Ph.D. student, McGill), internship at Parsifal (May - July)
• Salil Joshi (Ph.D. student, CMU), internship at Parsifal (June - August)
• Chris Martens (Ph.D. student, CMU), internship at Parsifal (June - August)

Visits

• Brigitte Pientka (McGill) visited Parsifal for a week during May
• Dale Miller (INRIA Saclay) visited McGill for three days in October. He participated in the Computer Science Colloquium.
• Dale Miller visited CMU for three days in October
• Kaustuv Chaudhuri (INRIA Saclay) visited CMU for a week in October
• Alberto Momigliano (Assistant Professor, Univ. of Milan) visited Parsifal for a week

Workshops and Seminars

• Summers @ LIX : sequence of seminars by participants of RAPT and other visitors, including talks by Rob Simmons (CMU) and Alwen Tiu (Australian National University)
• Kaustuv Chaudhuri co-organized the STRUCTURAL Workshop at LIX, March
• Kaustuv Chaudhuri gave a talk on Abella at the ETERNAL Workshop, October
• Dale Miller gave talks on Abella and related topics at the Computer Science Colloquium in McGill University and at CMU

Research Activities

The following is a summary of the work done in the RAPT project in 2011

1. Context management in Abella

Andrew Cave (intern @ Parsifal) worked on improving the treatment of contexts in Abella. Contexts in Abella are traditionally treated as lists which are sometimes endowed with particular inductive structures using inductive definitions. Working with such context definitions can often be cumbersome in practice. The goal of his work was to define standard regular specifications of contexts as seen in other systems such as Twelf and Beluga.

A prototype implementation of regular contexts was added to Abella. It is currently under review and will be incorporated into a future release of Abella.

2. Proof synthesis for G

Salil Joshi (intern @ Parsifal) worked on the problem of producing explicit proof representations from Abella. The main purpose of these proof objects is to increase our confidence in Abella proofs, but a secondary benefit is the possibility of exporting such proofs to other formal proof-development systems such as Coq or Agda.

There is an important theoretical question about how to certify completeness of sets of unifiers. Until this question is answered, it will not be possible to build a fully independent proof-checker for Abella. This is a matter of ongoing research.

3. Meta-theory of Type Systems

A number of type systems and meta-theoretic results were formalized in Abella, extending its library of examples.

• Andrew Cave formalized the Church Rosser proof for pure type systems (PTTs), which led to interesting observations about context management in Abella.
• Chris Martens (intern @ Parsifal) and Salil Joshi formalized the type-preservation proof for hereditary substitutions in the canonical lambda calculus.
• Chris Martens, Kaustuv Chaudhuri, and Dale Miller tried to formalize the mode and coverage checking operations of the Twelf proof assistant in Abella. This work has indicated a number of future avenues for research.

4. Future improvements in Abella

Abella in the future will probably have the following forks:

1. The “mainline” branch will remain roughly the same as the current version of Abella
2. A “linear” branch, called Abellin, will use a linear specification logic and allow for more expressive specifications of stateful and concurrent systems. A prototype implementation is expected to be released by the end of 2011.
3. A version of Abella with a richer type system is being planned for the near future. Its main purpose will be to formalize the meta-theory of LF as implemented by the Twelf system.

Additional Funding

INRIA

• Parsifal has had a successful ADT proposal to hire an engineer to co-ordinate the development of Abella. Quentin Heath was hired for this ADT for two years.

Canada

• Brigitte Pientka and Dale Miller were awarded a CPCFQ grant for French members to travel to Montreal
• Andrew Cave was supported by a Canadian scholarship during his internship

USA

• Chris Martens received an NSF REUSSI grant to travel to France for her interhship
• CMU partially supported Dale Miller’s visit in October

2012 Planning

These are the major themes of our planned research activities in 2012

• Package and release the improvements to Abella that were made in 2011 as Abella 2.0
• Integrate the Tac theorem prover with Abella as a special tactic
• New investigations into richer specification logics such as subexponential logic
• Carefully formalizing the mode, coverage, and termination checking components of Twelf in the two-level logic approach.

We plan to continue to host interns during the summer as it has been productive so far. We also plan to organize a RAPT workshop at LIX in 2012, possibly during the summer.