On computational interpretations of the modal logic S4. I. Cut elimination

A language of constructions for minimal logic is the
$\lambda$-calculus, where cut-elimination is encoded as
$\beta$-reduction. We examine corresponding languages for the
minimal version of the modal logic S4, with notions of reduction
that encodes cut-elimination for the corresponding sequent system.
It turns out that a natural interpretation of the latter
constructions is a $\lambda$-calculus extended by an idealized
version of Lisp's \verb/eval/ and \verb/quote/ constructs.

In this first part, we analyze how cut-elimination works in the
standard sequent system for minimal S4, and where problems arise.
Bierman and De Paiva's proposal is a natural language of constructions
for this logic, but their calculus lacks a few rules that are
essential to eliminate all cuts. The ${\lambda_{\rm S4}}$-calculus,
namelyBierman and De Paiva's proposal extended with all needed rules,
is confluent. There is a polynomial-time algorithm to compute
principal typings of given terms, or answer that the given terms are
not typable. The typed ${\lambda_{\rm S4}}$-calculus terminates, and
normal forms are exactly constructions for cut-free proofs. Finally,
... mehrmodulo some notion $\sqeq$ of equivalence, there is a natural
Curry-Howard style isomorphism between typed
${\lambda_{\rm S4}}$-terms and natural deduction proofs in minimal S4.

However, the ${\lambda_{\rm S4}}$-calculus has a non-operational
flavor, in that the extra rules include explicit garbage collection,
contraction and exchange rules. We shall propose another language of
constructions to repair this in Part II.