Paper on cut and explicit substitutions
Subject: Paper on cut and explicit substitutions
From: Rene Vestergaard <firstname.lastname@example.org>
Date: Thu, 23 Apr 1998 15:00:45 +0100 (BST)
Delivery-Date: Thu, 23 Apr 1998 09:03:28 -0500
I would like to announce the following paper on a Curry-Howard
correspondence between logics with cut elimination and calculi with
It is available in two versions:
(i) for public release, 12 pages, contains only outlines of proofs
(ii) author's cut, 50+ pages, with full proofs
The latter is also available in the technical report series of the Department
of Computing Science, University of Glasgow, (TR-1998-9).
--------------------- oOo ---------------------
The Cut Rule and Explicit Substitutions
University of Glasgow
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.