- Andrew Cave and Brigitte Pientka. “Programming with Binders and Indexed Data-types”, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2012, Philadelphia. (Cave was partially supported by RAPT during his internship in 2011, when this paper was written.)
- Beniamino Accattoli and Delia Kesner, “The Permutative Lambda-Calculus”. 18th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2012, Venezuela. (Accattoli travelled to LPAR on RAPT funds to present this work.)
- Alberto Momigliano: “A supposedly fun thing I have to do again: a HOAS encoding of Howe’s method”. 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), 2012, Copenhagen. (Momigliano’s paper uses several Abella extensions in development as part of RAPT; see Research Activities section below.)
- Beniamino Accattoli, “Proof pearl: Abella formalization of lambda-calculus cube property”, 2nd International Conference on Certified Programs and Proofs (CPP), 2012, Kyoto. (Accattoli was a postdoc at Parsifal when he wrote this paper on a novel proof technique in Abella.)
- Kaustuv Chaudhuri, “Compact Proof Certificates for Linear Logic”, 2nd International Conference on Certified Programs and Proofs (CPP), 2012, Kyoto.
- Yuting Wang (Ph.D. student, Univ. Minneapolis), internship at Parsifal (June - August)
- Beniamino Accattoli (postdoc, INRIA) visited McGill, Carnegie Mellon University, and the University of Brazil in March (funded in part by RAPT)
- Kaustuv Chaudhuri (researcher, INRIA) visited McGill and Univ. Minnesota for a week each in October (funded by RAPT)
- Quentin Heath (engineer, INRIA) visited McGill and Univ. Minnesota for a week each in October (funded by RAPT)
- Alberto Momigliano (professor, Univ. Milan) visited Parsifal at LIX in July
- Gopalan Nadathur (professor, Univ. Minnesota) visited Parsifal at LIX in July
- Brigitte Pientka (professor, McGill) visited Parsifal at LIX in February
- Fabien Renaud (postdoc, INRIA) visited McGill for a week in October
- Beniamino Accattoli finished his postdoc at Parsifal in October and continued to a two year postdoc position at Carnegie Mellon University under the mentorship of prof. Frank Pfenning.
Workshops and Seminars
- Brigitte Pientka gave a seminar on computation in dependently typed systems at Pi.R2 in Paris in February
- Beniamino Accattoli presented a paper at LPAR in Venezuela and gave a seminar on cost semantics of the lambda caluclus at the University of Brazil in March
- Kaustuv Chaudhuri, Quentin Heath, and Dale Miller (senior researcher, INRIA) participated in the workshop Proof Certificates and Computation at Copenhagen, Denmark in March
- Summers @ LIX : in July, Parsifal organised a workshop on computational reasoning tools with talks by both members of the RAPT project and by external collaborators (see “visits” above).
- David Baelde (asst. professor, ENS Cachan) visited Parsifal and spoke about his recent work on parity games and fixpoints.
- Kaustuv Chaudhuri co-organised the RAPT/Promis workshop on Proof Tools and Techniques at McGill during 15–17 October
- Kaustuv Chaudhuri, Quentin Heath, Gopalan Nadathur, Andrew Gacek (Rockwell Collins) and Yuting Wang participated in a focused development workshop on the Abella theorem prover in Univ. Minnesota during 22–26 October
The following is a summary of the work done in the RAPT project in 2012
1. Abella development and maintenance
The Abella theorem prover was built by Andrew Gacek (Rockwell Collins) in the University of Minnesota during his Ph.D. and subsequently during his postdoc at Parsifal. Since then, a number of other people have been building on his work in different branches of Abella, but the work has not been centrally co-ordinated. We have undertaken to create a developers and maintainers organisation for the continued future development of Abella.
The key aspects of this new organisation include:
- A new web-site, http://abella-prover.org
- Creation of a new GitHub organisation to centralise development of Abella
- The addition of Kaustuv Chaudhuri and Yuting Wang to the list of principal developers.
2. Generalising the Abella specification logic
The main product of Yuting Wang’s internship at Parsifal has been a nearly complete branch of Abella that extends the specification logic from second-order hereditary Harrop (HH2) formulas to arbitrary Lambda Prolog formulas (HH-omega). This extension substantially increases the expressive power of the specification logic, allowing a number of computational specifications in a simpler and more natural fashion.
A key ingredient in making the jump from HH2 to HH-omega was a focused treatment for the specification logic. Focusing is a very general mechanism for refining the structure of sequent proofs and thereby controlling the behaviour of proof search. It turns out that in the HH-omega proof theory, it is sometimes essential to reason about program fragments in contexts of object sequents; focusing is critical in representing such reasoning paths. Moreover, all existing HH2 theorems continue to hold in the extension to focused HH-omega, although some proofs have to be slightly modified for the new focused setting.
The HH-omega branch of Abella has been demonstrated at a workshop in LIX in July and then subsequently at the RAPT/Promis workshop in Montreal in October. Several changes were implemented in response to feedback from users and this branch has been scheduled to be incorporated into the mainline of Abella in the upcoming 2.0 release.
Wang and Chaudhuri are in the process of writing a paper documenting this branch of Abella.
3. Polymorphic types in Abella and Bedwyr
Abella has historically supported only a simple type system based on Church’s Simple Theory of Types. While this has been adequate for small problems, it is clear that for larger developments one would require some support for polymorphism. Our colleagues at the University of Minnesota (Gopalan Nadathur, Yuting Wang, Mike Whalen) and at Rockwell Collins (Andrew Gacek) have been using Abella to formally show the correctness of a compiler for a synchronous dataflow programming language used for programming reactive systems in such domains as avionics and nuclear power plants. Their work is greatly hindered by the lack of polymorphism in Abella.
A common example of the need for polymorphism in such large scale projects has to do with composing data. Currently in Abella, if we need two kinds of lists, the only option is to give two different definitions and duplicate all relevant lemmas about lists for these separate definitions. The problem quickly worsens with increasing structure in the data – for instance, a list of pairs of natural numbers would not only require special lemmas about numbers, pairs, and lists, but also lifting lemmas to move the results from numbers to pairs of numbers, and then to lists of pairs of numbers.
We have undertaken to extend the type system of Abella to support polymorphic types and polymorphic lemmas. Our type system is inspired by the parametric polymorphism of programming languages such as ML and Haskell. Most of the development has been straightforward as the issues with polymorphic type-inference are well known. The implementation is scheduled to be included in the mainline 2.0 release of Abella.
The main theoretical issue with polymorphism in Abella has been the treatment of subordination. Consider the following signature:
kind tm, ty type. type b ty. type arr ty -> ty. type abs (tm -> tm) -> tm. type app tm -> tm -> tm.
From this signature, if we were to compute the subordination relation,
we would deduce neither that
tm is subordinate to
ty, nor the
converse. That is to say, in normal ground terms of type
can be no occurrences of subterms of type
tm. Hence, whenever we
have a function of type
tm -> ty, we can immediately conclude that
it ignores its argument; this can be used to prune dependencies in
metavariables and lead to more equations falling into the dynamic
L-lambda fragment which is amenable to higher-order unification.
This simple situation is complicated with the introduction of polymorphic types. Consider the following addition to the signature.
type fst A -> B -> A.
One valid interpretation of such a declaration is that the type of
(fst U V) is independent of the type of
V. Hence, the following
normal term of type
arr (fst b (abs x\ x)) b
contains a strict subterm,
abs x\ x, of type
tm. This means that
the complement of the subordination relation becomes empty, making the
computation of this relation completely pointless.
As the subordination relation is very useful in practice, we choose to
disallow declarations such as
fst from signatures. Practically, this
amounts to the following restriction: the target type of any
signature constant must contain all the type variables in the type of
the constant. Since the target type of
A, does not
contain the variable
B, it fails the check and is disallowed. Note
that we can still declare polymorphic constants such as the following.
type id A -> A. type nil list A. type cons A -> list A -> list A. type mkpair A -> B -> pair A B.
Lambda Prolog, which is the basis for the specification logic of Abella, has a very general notion of polymorphism that includes both parametric polymorphism and ad hoc polymorphism. Supporting reasoning about the full generality of the Lambda Prolog type system, especially in the presence of induction, co-induction, and subordination, is essentially an open research problem lacking good answers. Fortunately, supporting the full generality of Lambda Prolog’s type system is not urgent.
4. Towards a more robust proof language for Abella
One of the most questionable aspects of Abella from a trust perspective is that the proof tactics are trusted. That is, there is no independently verifiable proof object for an Abella theorem. During 2011 we investigated the fundamental problem of certifying Abella proofs, but came to the conclusion that producing a truly independent proof output from Abella was difficult because of the open theoretical problem of certifying completeness of a set of unifiers for a higher-order unification problem.
From a pragmatic perspective, we can improve the trustworthiness of Abella proofs with a slightly weaker notion of trust by treating the unification engine of Abella as a trusted component. Indeed, this definition of trust has already been adopted by the ProofCert project at Parsifal. An interesting aspect for this notion of trust is that we can make the proof language of Abella more robust; this will be the major focus of RAPT activities in 2013. Briefly, Abella proofs are now closely linked to the operational semantics of Abella’s unification engine. For case-analysis, the cases in the proof must be in precisely the order that they are generated by the implementation of higher-order unification, which is not fully predictable from the text written by the user. We are instead planning to decouple the presentation of cases as the user writes them from the check that they cover all the possibilities required by unification. This will bring the Abella proof language more in line with coverage-based approaches in systems such as Twelf or Beluga.
5. A theory of contexts
An emerging theme in the work on Abella, Beluga, and some related systems such as Hybrid, is a way to abstract common idioms in the treatment of contexts in computational specifications. Currently, each system has strengths the others lack. In Abella, contexts can be given very general relational specifications, but the user has to repeatedly prove lemmas about elements in contexts. Beluga on the other hand makes reasoning on the structure of contexts mostly automatic, but it can only handle a single regular context, and the meta-theory of contexts tends to be complicated. In an ideal world, we would be able to take the regular context schemas in the Beluga style—together with the automated reasoning about such contexts—to specify contexts in Abella in the cases where they suffice, while allowing the user to fall back to the fully general relational definitions when necessary.
There are both theoretical and practical challenges to this ideal picture. The theory of regular contexts, although well developed, does not yet give a logical account of the structural features of contexts, in particular of subsumption, weakening, and strengthening. The main issue is that some structural rules such as weakening are height-preserving, meaning that they should not affect the applicability of inductions on the structure of derivations, while other rules such as strengthening need not be height-preserving. Currently, all the above systems lack a means of expressing the height-preserving nature of context transformations.
From a practical standpoint, the key question is whether regularity of contexts is something the system detects and then handles transparently, or if it is something the user explicitly annotates in his definitions. Both approaches come with trade-offs. If the system infers regularity, then the implementation becomes more complex (and therefore less trustworthy), and the user might be surprised by the system discharging proof obligations that he had expected to write proofs for explicitly. In the alternative, the system would have two different ways to specify the same things, so the user might be confused about which style is to be used in which situations.
A careful comparison of the three systems with regard to the treatment of contexts is being undertaken by Brigitte Pientka, Amy Felty (professor, Univ. of Ottawa), and Alberto Momigliano (professor, Univ. Milan).
6. The expressive reach of the two-level logic approach
Systems such as Abella and Beluga implement a strict nesting of specification logics inside reasoning logics (or computations, in the case of Beluga). While this strict nesting is usually sufficient, there are some domains where this restriction is too limiting. To illustrate, in Abella it is currently impossible to use negation in the specification logic, so it is not possible to write a definition such as:
normal (abs M) :- pi x\ normal x => normal (M x). normal (app M N) :- normal M, normal N, (pi U\ not (M = lam U)).
normal M would succeed iff
M is a normal lambda
expression. Unfortunately, Abella does not support the
in the specification logic. Therefore, the
normal relation in Abella
needs to be written in the following more cumbersome fashion, using an
normal (abs M) :- pi x\ neutral x => normal (M x). normal M :- neutral M. neutral (app M N) :- neutral M, normal N.
There are essentially two ways to handle this deficiency. One is to augment the two-level logical basis of Abella to admit negation at the specification level, but if done naively then the provability relation in the reasoning logic (the logical basis of the curly-braces of Abella) can become non-stratified. A less drastic approach would be to allow the specification logic to appeal to certain predicate symbols, such as equality and negation, in the reasoning logic. That is to say, the second clause of the above definition might be written as:
normal (app M N) :- normal M, normal N, (pi U\ [[ M = lam U -> false ]]).
[[ ]] is used to embed a reasoning-level formula into the
There are a number of other examples where a limited amount of appeal to reasoning logic predicates in the specification logic seems to be either necessary or very useful. We are currently exploring the meta-theory of this kind of back-and-forth communication between the two logics.
7. Interactions between Abella and Bedwyr
Bedwyr is a model checker for sophisticated specifications
in a logic very similar to the reasoning logic of Abella. Unlike
Abella, Bedwyr cannot be used to prove inductive theorems; even
trivial theorems such as
nat M -> nat M are beyond the scope of
Bedwyr because the way it attempts to prove it is by first
constructing the full set of terms
M for which
nat M holds, which
is infinite. On the other hand, Bedwyr is very efficient at
exhaustively checking a finite search space because it is based on
tabled search; Abella, by comparison, has only a rudimentary search
engine that does not attempt to reason by unfolding definitions.
A recent effort by Quentin Heath (engineer at Parsifal) and Dale Miller (senior researcher at Parsifal) has been to combine the strengths of the two systems in the following manner: Abella would be used to prove inductive lemmas about a Bedwyr specification, and Bedwyr would then use these lemmas to improve its tabling mechanism and prune the search space further. A simple example of this approach is a specification of Tic Tac Toe, where Bedwyr can find winning strategies fully automatically; unfortunately, it is not possible to ask Bedwyr to prove that when a board is a winning position for a player, then all symmetric versions of the board also are winning positions. Thus, Bedwyr will end up re-deriving that a symmetric board is or is not a winning position. However, symmetry theorems are fairly straightforward to prove in Abella.
The Abella and Bedwyr languages have been modified slightly so that the same file containing a Bedwyr specification and an Abella proof can be accepted by both systems. Abella would only check the inductive proofs in the file, while Bedwyr would use the lemmas to improve its handling of queries. This is part of the focus of the ADT BATT (2011-2013).
- Matteo Cimini was hired as a postdoc at Parsifal for one year as part of the INRIA postdoc compition in 2012; his work is strongly related to the topics of RAPT (Abella and structured operational semantics).
- Yuting Wang: internship was partially funded by matching funds from the DRI, separate from RAPT funds.
- Brigitte Pientka (McGill) was awarded a grant by the commission permanente de coopération franco-québécoise (CPCFQ, 63rd session, 2011–2012) and the PSR-SIIRI (2011-2013) for the project Promis : de la théorie des preuves à la pratique de la démonstration automatique. Dale Miller (Parsifal), Frank Pfenning (Carnegie Mellon University), Gopalan Nadathur (Univ. Minnesota), and Iliano Cervesato (Carnegie Mellon University Qatar Campus) are listed as principal international collaborators. The funding was for the maximum amount of 150,000 CAD over three years, and will be mainly spent on Ph.D. students and postdocs at McGill.
- Beniamino Accattoli was awarded a post-doctoral fellowship for two years (2012–2014) through the Meta CLF project at Carnegie Mellon University.
- Yuting Wang: NSF through the REUSSI program paid for his plane tickets
- Univ. Minnesota: Gopalan Nadathur has advertised a 1 year postdoc position for working on Abella, funded by the NSF
In 2013 we plan to do the following:
Continue the various strands of work outlined in the Research Activities section above.
Host an intern from McGill (we have a candidate in mind already) during summer 2013, and possibly another intern from Carnegie Mellon or Univ. Minnesota.
Organise a workshop on computational logic tools at LIX, either as part of the LIX colloquium in 2013 (also being organised by Parsifal) or as a separate workshop.
Organise a meeting of Abella developers at either McGill, CMU, or Univ. Minnesota to coordinate future development and deployment of Abella. We plan to send 3–4 Parsifal team members to such a meeting.
We expect to make use of the full budget allocated to third year EAs (10K euros).