# Paper on cut and explicit substitutions

• To: types@cs.indiana.edu
• Subject: Paper on cut and explicit substitutions
• From: Rene Vestergaard <jrvest@dcs.gla.ac.uk>
• Date: Thu, 23 Apr 1998 15:00:45 +0100 (BST)
• Delivery-Date: Thu, 23 Apr 1998 09:03:28 -0500

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.