INRIA EA RAPT Report 2011




Workshops and Seminars

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.

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





2012 Planning

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

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.