Proof theory for term representations


Dale Miller, Parsifal team, INRIA-Saclay and LIX/Ecole Polytechnique

Description du sujet

Basic to the construction of any symbolic system is the structure terms, which are used to represent expressions, programs, formulas, types, etc. One way to define the structure of terms is as small proofs of their types. Such a view of terms provides a direct way to model substitutions as well bindings within terms. For example, a common representations of λ-terms uses the head normal form of terms where every (normal) term has the structure

(λ x1 ... λ xi. h t1 ... tj),

where h (the head of the term) is a variable or constant, t1, ..., tj are head normal terms (the arguments), and x1, ..., xi are variables bound in the body of this term (the binder). This structure for terms corresponds to particular cut-free proofs---variously called uniform proofs or LJT proofs---of implicational formulas viewed as types. Given that "terms are proofs", the encoding and dynamics of substitution can be addressed by using cut and cut-elimination.

One drawback of the head-normal form structure of λ-terms is that they do not have direct support for either sharing or parallel structure in terms. Direct support for sharing makes it possible to have much more compact encodings of some structures than is provided by the head normal form, which requires copying and recopying the same substructure. However, sharing appears to have its own problems: Can sharing in terms be enforced? Can sharing persist during substitutions and normalizations? Can sharing help or hinder operations on terms structures such as equality checking and unification?

Recent advances in proof theory related to focused proofs systems should have immediate application to these issues of term representation. Some of these recent advances include:

The purpose of this internship is to address some of these issues in term representation by making use of the recent results in focusing proof systems.

This internship will take place within the funding context of the ProofCert project (an ERC Advanced Grant). This five year project (2012-2016) provides funding for PhD students covering a broad range to topics in a foundational approach to proof certificates. Continuing to work on this topic for a PhD is possible and encouraged.


The following bibliography is indicative of the kind of papers that will be part of this research effort.

A multi-focused proof system isomorphic to expansion proofs by Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. Accepted to the J. of Logic and Computation: pdf.
LJQ: A Strongly Focused Calculus for Intuitionistic Logic by Roy Dyckhoff and Stéphane Lengrand. CiE 2006: 173-185: pdf.
Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Theoretical Computer Science, 410(46), pp. 4747-4768 (2009): pdf.
Completing Herbelin's Programme by José Espírito Santo. TLCA 2007: 118-132: pdf.

Dale Miller