Applying Recent Advances in Proof Theory to Specification and Reasoning
The RAPT project was an INRIA Associated Team (Equipe Associée) that ran during 2011–2013.
Background
Many aspects of computation systems, ranging from operational semantics, interaction, and various forms of static analysis, are commonly specified using inference rules, which themselves are formalized as theories in a logical framework. While such a use of logic can yield sophisticated, compact, and elegant specifications, formal reasoning about these logic specifications presents a number of difficulties. The RAPT project will address the problem of reasoning about logic specifications by bringing together three different research teams, combining their backgrounds in type theory, proof theory, and the building of computational logic systems. We plan to develop new methods for specifying computation that allow for a range of specification logics (eg, intuitionistic, linear, ordered) as well as new means to reason inductively and co-inductively with such specifications. New implementations of reasoning systems are planned that use interactive techniques for deep meta-theoretic reasoning and fully automated procedures for a range of useful theorems.
Documents
Publications
- Beniamino Accattoli and Delia Kesner, “The Permutative Lambda-Calculus”. 18th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2012, Venezuela.
- 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.
- Beniamino Accattoli, “Proof pearl: Abella formalization of lambda-calculus cube property”, 2nd International Conference on Certified Programs and Proofs, 2012, Kyoto.
- Kaustuv Chaudhuri, “Compact Proof Certificates for Linear Logic”, 2nd International Conference on Certified Programs and Proofs, 2012, Kyoto.
- 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.
Activity Reports
People
INRIA Saclay - Île-de-France
- Kaustuv Chaudhuri (CR INRIA, PI)
- Matteo Cimini (Postdoc, INRIA)
- Quentin Heath (Engineer)
- Dale Miller (DR INRIA)
McGill University
- Andrew Cave (Ph.D. student)
- Brigitte Pientka (Professor, PI)
- Olivier Savary-Bélanger (Masters student)
Carnegie Mellon University
- Beniamino Accattoli (Postdoc)
- Salil Joshi (Ph.D. student)
- Chris Martens (Ph.D. student)
- Frank Pfenning (Professor)
University of Minnesota
- Gopalan Nadathur (Professor)
- Yuting Wang (Ph.D. student)
Software
- Abella, an interactive theorem prover
- Bedwyr, a sophisticated model checker
- RAPT Gforge Project