[Prev][Next][Index][Thread]

Paper on cut and explicit substitutions

Dear Colleagues,

  I would like to announce the following paper on a Curry-Howard
correspondence between logics with cut elimination and calculi with
explicit substitution.

It is available in two versions: 
   (i) for public release, 12 pages, contains only outlines of proofs
       http://www.dcs.gla.ac.uk/~jrvest/Writings/CSL98.ps.gz
  (ii) author's cut, 50+ pages, with full proofs
       http://www.dcs.gla.ac.uk/~jrvest/Writings/cut-ExplSubst-long.ps.gz
The latter is also available in the technical report series of the Department
of Computing Science, University of Glasgow, (TR-1998-9).

Regards
/R

    --------------------- oOo ---------------------

        The Cut Rule and Explicit Substitutions
                   Rene' Vestergaard
                 University of Glasgow

                       ABSTRACT

We construct two \lambda-like calculi with explicit substitutions
isomorphic to two Gentzen style logical deduction (sequent calculus)
logics and constructive proofs of their Haupts\"atze. We thus expound
the view, that cut elimination under the Curry-Howard Correspondence
is propagation of explicit substitutions.

By seeing the constructed calculi as non-overlapping term rewriting
systems (i.e., without critical pairs), we strengthen the Haupts\"atze
through an equivalence result between weak innermost normalisation and
strong normalisation due to Gramlich.

We formally relate the constructed calculi to \lambda s and \lambda t,
two well-studied explicit-substitution calculi a` la de Bruijn. We
show that the substitution (index-updating) mechanisms of the latter
two coincide with the cut (weakening) rules of the logics in question.

A meta-level treatment of the dereliction rule introduces a garbage
collection rule for both calculi a` la \lambda xgc.