## Patrick Baillot and Marco Pedicini.
Elementary complexity and geometry of interaction.
*Fund. Inform.*, 45(1-2):1-31, 2001.
Typed lambda calculi and applications (L'Aquila, 1999).

We introduce a geometry of interaction model given by
an algebra of clauses equipped with resolution
(following citeGirard95d) into which proofs of
Elementary Linear Logic can be interpreted. In order to
extend geometry of interaction computation (the so
called *execution formula*) to a wider class of
programs in the algebra than just those coming from
proofs, we define a variant of execution (called *
weak execution*). Its application to any program of
clauses is shown to terminate with a bound on the
number of steps which is elementary in the size of the
program. We establish that weak execution coincides
with standard execution on programs coming from proofs.

[ bib |
.ps ]

Back

*This file has been generated by
bibtex2html 1.60*
>>> BackToHomePage(Protocollo) <<<