
V.Danos, M.Pedicini, L.Regnier Directed Virtual Reductions, In
M.Bezem D.van Dalen, editor, Computer Science Logic, 10th International
Workshop, CSL '96, volume 1258 of Lecture Notes in Computer Science,
pages 7688. EACSL, Springer Verlag, 1997. [format postscript or gzipped
postscript].
ABSTRACT: This
note defines a new graphical local calculus, \emph{directed virtual reductions}.
It is designed to compute Girard's execution formula \EX, an invariant
of closed functional evaluation obtained from the ``geometry of interaction''
interpretation of $\lambda$calculus \cite{Girard88a}. The calculus is
obtained by synchronizing another graphical local calculus presented in
``local and asynchronous betareduction'': \emph{virtual reductions} \cite{DanosRegnier93}.
This synchronization makes it easier to mechanize than general virtual
reductions. In undirected virtual reductions the consistency of the computation
is insured by an algebraic mechanism called the \emph{bar}. This mechanism
in general induces correction terms of any order. The directed virtual
reduction has been designed to keep those terms at order one. A further
synchronization, the \emph{combustion strategy} will even wipe out first
order correction terms. Applied to sharing graphs, the combustion strategy
yields Lamping's optimal graphical calculus as presented in \cite{AbadiGonthierLevy92a}.
But more efficient optimal implementations of $\lambda$calculus are expected.
The paper is conceived as a followup of \cite{DanosRegnier93} and supposes
a familiarity with virtual reduction.

P.Loreti, M.Pedicini, An Idempotent Analogue of Resolvent Kernels
for a Deterministic Optimal Control Problem Technical Report IAC
n.16 1996. [format gzipped
postscript].
ABSTRACT: In
this paper we investigate the discretized HamiltonJacobiBellman equation
by formulating it in the idempotent semiring of real numbers with operations
min and +. It results to be the idempotent analogue of the Volterra integral
equation of second type and it can be approximated by the method of the
resolvent kernel.

M.Pedicini, Remarks on Elementary Linear Logic, in Electronic
Notes in Theoretical Computer Science Volume 3, A Special Issue on the
"Linear Logic 96, Tokyo Meeting" [format postscript].
ABSTRACT: Last
works in linear logic mark a trend that can be summarized as: studying
of fragments of calculi which have good logical properties and a quite
powerful class of representable functions. ELL is a system derived from
linear logic which presents several of such good properties: first of all
a bound of the cutelimination procedure which is lower w.r.t. the usual
one.

F.Costantini, G.F.Mascari, M.Pedicini, Dynamics of Algorithms
Technical Report IAC n.6 1996 [format gzipped
postscript].
ABSTRACT: A
challenge problem in studying complex systems is to model internal structure
of the system and its dynamical evolution in an integrated view. An algorithm
computes a function with domain consisting of all its possible inputs and
as codomain all possible outputs. In order to ''compare'' algorithms computing
the same function (e.g. with respect to time or space complexity) it is
necessary to model the ''dynamic behavior'' of the algorithm. The main
approach for modeling the dynamic behavior $Bh({\bf P})$ of an algorithm
is ''the dynamic system paradigm'': $Bh({\bf P})$ is obtained as the action
of a (control) monoid on a (state) space. Various mathematical structures
have been considered for attacking such a problem; among others, deterministic
automata and stochastic automata. In order to capture the fine structure
of computation, recently an attempt to describe the ''macroscopic'' global
dynamic behavior of an algorithm in terms of the ''microscopic'' local
dynamic behavior of its components has been proposed within a logical approach
to computing called ''Geometry of Interaction'' developed within $C^{*}$algebras.
We propose an algebraic approach to ``structured dynamics'' inspired by
the Geometry of Interaction and based on a ''many objects'' generalization
of semirings: partially additive categories.

M.Pedicini, G.Pontrelli, Symbolic
Calculus in NonNewtonian Fluid Mechanics Technical Report IAC
n.4 1996.
ABSTRACT: A
general purpose package in Mathematica environment for the automatic computation
of nonnewtonian flow equations is developed and presented. The software
allows the user to chose among three coordinate systems and four different
fluid models. Changing of variables, scaling and other formal manipulation
of the equations are also possible.

G. F. Mascari, M. Pedicini, Types
and Dynamics in Partially Additive Categories , in "Idempotency"
, Ed. J.Gunawardena, Publications of the Isaac Newton Institute, vol. 11.
Cambridge University Press (1998).
ABSTRACT: In
this paper we present a general view of structural dynamics inspired by
proof theory. The execution of pseudoalgorithms defined in the framework
of partially additive categories is given as a kind of iteration of endomorphisms.
We also consider deadlock free pseudoalgorithms as to be characterized
by a summability condition and the theorem stating modularity with respect
to dynamics is proved. Finally in the last section, concepts about structural
aspects are organized via type discipline and type compatible dynamics.

G.F. Mascari,M.Pedicini, Head
Linear Reduction and Pure Proof Net Extraction, in TCS 135 (1994)
111137.
ABSTRACT: Proof
net calculus introduced in [Gir86] has been extended in the paradigm of
the Scott's domains equation D = D > D which generates a logical point
of view for pure lambdacalculus in [Dan89]. Methodologically speaking:
in this paper the proof theoretic counterpart of the Böhm's Theorem
given in [Boh68] for pure lambdacalculus, is proposed as extention of
the CurryHoward paradigm. Tecnically speaking: as the extraction of a
subterm using the betareduction is possible also subnet extraction can
be internalized by cutelimination: using proof nets helps us to understand
more deeply, and to handle in a better way the procedure of extraction.

M.Pedicini, Schémas
Principaux et Réseaux de Preuves, Memoire de DEA, Univ.
Paris VII.
ABSTRACT: Dans
[Gir86] on peut trouver la definition des reseaux pour la logique lineaire,
Vincent Danos et Laurent Regnier [Dan89] ont montre comment on peut traduire
le lambda calcul pur dans un cas particulier des reseaux du fragment multiplicatif
avec exponentielles (notamment la ou on voit que il n'y a que les formules
I,O,!I,?O a cause de l'equation au point fixe D=D > D du lambdacalcul
pur et des lois de De Morgan valides pour les connecteures de la logique
lineaire). Ici on introduit un formalisme different pour les reseaux normaux
et on demontre que ces reseaux correspondent aux types principaux dans
le systeme D(Omega). Les resultats contenus dans ce memoire sont dus au
travail de Jacques Van de Wiele et Eric Duquesne.