Papers by Lorenzo Tortora de Falco

 Lorenzo Tortora de Falco
Generalized standardization lemma for the additives
(postcript)
Electronic Notes in Theoretical Computer Science, Volume 3, Elsevier 1996.
ABSTRACT:
This is a preliminary report, in which we prove the
socalled standardization lemma for the additives, in presence
of a generalization (the natural one) of the commutative
elementary reduction step. The technical tools developped to
achieve this result suggest some remarks on the non confluence of
full linear logic (without constants).

 Myriam Quatrini, Lorenzo Tortora de Falco
Polarisation des preuves classiques et renversement
(postcript)
CompteRendu de l'Académie des Sciences Paris,
t.323, Série I, p.113116, 1996.
ABSTRACT:
We introduce a new constraint on the proofs of the classical sequent
\hspace{6em} calculus $LK^\eta_{pol}$ ($\eta$constrained and polarized). We
obtain a complete and
\hspace{6em} stable fragment for which the $P$ embedding into linear logic is
a decoration.

 JeanBaptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco
Strong Normalization for `allstyle' $LK^{tq}$
(postscript )
Lecture Notes in Artificial Intelligence 1071,
p. 226243, SpringerVerlag 1996.
ABSTRACT:
We prove strong normalization of $tq$reduction for all standard versions
of sequent calculus for classical and intuitionistic (first and second order)
logic and give a perspicuous argument for the completeness of the focusing
restriction on sequent derivations.

 Lorenzo Tortora de Falco
Denotational semantics for polarized (but nonconstrained) $LK$
by means of the additives
(postscript )
Lecture Notes in Computer Science,
1289 pp. 290304 special issue
for the proceedings of the conference ``$5^{th}$ Kurt Goedel Colloquium
KGC'97, computational logic and proof theory", Wien (Austria) 2529
august 1997, SpringerVerlag 1997.
ABSTRACT:
Following the idea that a classical proof is a superimposition
of `constructive' proofs, we use the linear connective ``$\&$'' to
define an embedding $P^a$ of polarized but nonconstrained $LK$
in linear logic, which induces a denotational semantics.
A classical cutelimination step is now a cutelimination step
in one of the `constructive slices' superimposed by the classical proof.

 Lorenzo Tortora de Falco
Réseaux, cohérence et expériences obsessionnelles
(postscript )
PhD thesis, Université Paris 7,
january 2000.
ABSTRACT:
You can look at the table of contents

 Lorenzo Tortora de Falco
Coherent obsessional experiments for Linear Logic proofnets
(pdf )
The Bulletin of Symbolic Logic volume 7, Issue 1, p.154, march 2001.

 Lorenzo Tortora de Falco
Additives of linear logic and normalization Part I: a
(restricted) ChurchRosser property
( postscript )
Theoretical Computer Science 294/3
pp. 489524, february 2003.
ABSTRACT:
We define a generalized cutelimination procedure for proofnets
of full linear logic (without constants), for which we prove
a (restricted) ChurchRosser property.

 Lorenzo Tortora de Falco
Additives of linear logic and normalization Part II: the additive
standardization theorem
(postscript )
preprint Quaderno I.A.C.C.N.R. n. 10/2001,
and submitted for publication.
ABSTRACT:
We prove the additive standardization theorem for full linear logic
(without constants).

 JeanBaptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco
SN and CR for freestyle LKtq: linear decorations and
simulation of normalization
( postscript ),
The Journal of Symbolic Logic 67 (1), march 2002,
pp. 162196
ABSTRACT:
The present report is a, somewhat lengthy, addendum to~\cite{DanJoiSche97}, where
the elimination of cuts from derivations in sequent calculus for classical logic
was studied `from the point of view of linear logic'. To that purpose a formulation
of classical logic was used, that  as in linear logic  distinguishes between
{\em multiplicative}\/ and {\em additive}\/ versions of the binary connectives.
The main novelty here is the observation that this {\em
typedistinction}\/ is not essential: we can allow classical sequent
derivations to use {\em any}\/ combination of additive and
multiplicative introduction rules for each of the connectives, and
still have strong normalization and confluence of $tq$reductions.
We give a detailed description of the simulation of $tq$reductions by
means of reductions of the interpretation of any given classical proof
as a proof net of {\bf PN2} (the system of second order proof nets for
linear logic), in which moreover all connectives can be taken to be of
{\em one}\/ type, e.g.\ multiplicative.
We finally observe that dynamically the different logical cuts, as determined
by the four possible combinations of introduction rules, are {\em independent}:
it is not possible to simulate them {\em internally}, i.e.\ by only {\em one}\/
specific combination, and structural rules.

 Olivier Laurent, Myriam Quatrini, Lorenzo Tortora de Falco
Polarized and focalized classical and linear proofs
(preliminary version in postscript ),
Annals of Pure and Applied Logic 134,
Issues 23, pp. 217263, july 2005
ABSTRACT:
We give the precise correspondence between polarized linear
logic and polarized classical logic. The properties of focalization
and reversion of linear proofs \cite{AndrPar,lc,lktq}
are at the heart of our analysis: we show that the \tqprotocol of
normalization (defined in \cite{lktq}) for the classical systems
\LKe{} and \LKer{} perfectly fits normalization of polarized proofnets.
In section~\ref{isos}, some more semantical considerations allow
to recover \LC{} as a refinement of multiplicative \LKe.

 Lorenzo Tortora de Falco
The additive multiboxes
( postscript ),
Annals of Pure and Applied Logic 120, 13 pp. 65102, january 2003
ABSTRACT:
We introduce the new notion of additive ``multibox'' for
linear logic proofnets. Thanks to this notion, we define
a cutelimination procedure
which associates with every proofnet of multiplicative
and additive linear logic a unique cutfree one.

 Lorenzo Tortora de Falco
Obsessional experiments for Linear Logic Proofnets
(preliminary version in
postscript ),
Mathematical Structures in Computer Science
13, (Issue 6) pp. 799  855, december 2003
ABSTRACT:
We address the question of injectivity of coherent semantics of
linear logic proofnets.
Starting from the definition of experiment
given by Girard, we introduce the keynotion of ``injective obsessional
experiment'', which allows to give a positive answer to our question
for certain fragments of linear logic, and to build counterexamples to the
injectivity of coherent semantics in the general case.

 Olivier Laurent, Lorenzo Tortora de Falco
Slicing polarized additive normalization
( postscript )
London Mathematical
Society Lecture Note Series volume 316, pp. 247282
Cambridge University Press 2004 (Book having as title "Linear Logic in
Computer Science", Thomas Ehrhard, JeanYves Girard,
Paul Ruet and Phil Scott editors)
ABSTRACT:
To attack the problem of ``computing with the additives'',
we introduce a notion of sliced proofnet for the
polarized fragment of linear logic.
We prove that this notion yields computational objects,
sequentializable in the absence of cuts.
We then show how the injectivity property of denotational semantics
guarantees the ``canonicity'' of sliced proofnets, and prove injectivity
for the fragment of polarized linear logic corresponding to simply typed
lambdacalculus with pairing.

 Lorenzo Tortora de Falco
Sulla struttura logica del calcolo
( pdf )
Rendiconti di Matematica e delle sue Applicazioni. vol. VII (26), 2006
ABSTRACT:
Proponiamo una rassegna di alcuni aspetti degli sviluppi recenti della teoria della dimostrazione e dei suoi legami con l'informatica.

 Olivier Laurent, Lorenzo Tortora de Falco
Obsessional cliques: a semantic characterization of bounded time complexity
( postscript )
IEEE Computer Society
Twentyfirst annual IEEE symposium
on Logic In Computer Science (LICS '06). August 2006.
ABSTRACT:
We give a semantic characterization of bounded complexity proofs.
We introduce the notion of obsessional clique in the relational model
of linear logic and show that restricting the morphisms of the category
REL to obsessional cliques yields models of ELL and SLL.
Conversely, we prove that these models are relatively complete: an
LL proof whose interpretation is an obsessional clique is always an
ELL/SLL proof. These results are achieved by introducing a
system of ELL/SLL untyped proofnets, which is both correct
and complete with respect to elementary/polynomial time complexity.

 Michele Pagani, Lorenzo Tortora de Falco
Strong normalization property for second order linear logic
( pdf )
Theoretical Computer Science volume 411, issue 2, pp. 410444, january 2010.
ABSTRACT:
The paper contains the first complete proof of strong normalization (SN) for full second order linear logic (LL): Girard's original proof uses a standardization theorem which is not proven.
We introduce sliced pure structures (sps), a very general version of Girard's proofnets, and we apply to sps Gandy's method to infer SN from weak normalization (WN). We prove a standardization theorem for sps: if WN without erasing steps holds for an sps, then it enjoys SN. A key step in the proof of standardization is a confluence theorem for sps obtained by using only a very weak form of correctness, namely acyclicity slice by slice.
We conclude by showing how standardization for sps allows to prove SN of LL, using as usual Girard's reducibility candidates.

 Daniel De Carvalho, Michele Pagani, Lorenzo Tortora de Falco
A semantic measure of the execution time in Linear Logic
( pdf )
Theoretical Computer Science volume
412, issue 20, pp. 18841902, april 2011.
ABSTRACT:
We give a semantic account of the execution time (i.e. the number of cutelimination steps leading to the normal form) of an untyped MELL (proof)net. We first prove that: 1) a net is headnormalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then define a size on every experiment of a net, and we precisely relate the number of cutelimination steps of every stratified reduction sequence to the size of a particular experiment. Finally, we give a semantic measure of execution time: we prove that we can compute the number of cutelimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the (untyped) lambdacalculus.

 Daniel De Carvalho, Lorenzo Tortora de Falco
The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)
( pdf ) and a little
Erratum
( pdf )
Annals of Pure and Applied Logic Volume 163, Issue 9, pp. 12101236, september 2012.
ABSTRACT:
We show that for a suitable fragment of linear logic the syntactical equivalence relation on proofs induced by cutelimination coincide with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. More precisely, we prove that two cutfree proofs of the multiplicative and exponential fragment of linear logic with the same interpretation in the multiset based relational model are the same ``up to the connections between the doors of exponential boxes''. This result is proven in an untyped framework: two cutfree untyped ProofStructures (PS) have the same Linear ProofStructure (LPS). An immediate consequence is that two cutfree PS without weakenings with the same relational interpretation are the same; hence relational semantics is injective.

 Pierre Boudes, Damiano Mazza, Lorenzo Tortora de Falco
An Abstract Approach to Stratification in Linear Logic
( pdf )
Information and Computation Volume
241, pp. 3261, april 2015.
ABSTRACT:
We study the notion of stratification, as used in subsystems of
linear logic with low complexity bounds on the cutelimination
procedure (the socalled light logics), from an abstract point of
view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is
a generalization of the paragraph modality of Girard's light linear
logic, arises from a general categorical construction applicable to
all models of linear logic. We thus learn that stratification may be
formulated independently of exponential modalities; when it is
forced to be connected to exponential modalities, it yields
interesting complexity properties. In particular, from our analysis
stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic.

 Daniel de Carvalho, Lorenzo Tortora de Falco
A semantic account of Strong Normalization in Linear Logic
( pdf )
Information and Computation Volume
248, pp.104129, june 2016.
ABSTRACT:
We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly normalizable) compute the maximal length of the reduction sequences starting from that net.

 Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco
Computing connected proof(structure)s from their Tayolr expansion
( pdf )
to appear in Leibniz International Proceedings in Informatics (LIPIcs) proceedings of the conference ``Formal Structures for Computation and Deduction'', Porto (Portugal), 2225 june 2016
ABSTRACT:
We show that every connected Multiplicative Exponential Linear Logic (MELL)
proofstructure (with or without cuts) is uniquely determined by a wellchosen
element of its Taylor expansion: the one obtained by taking two copies of the
content of each box. As a consequence, the relational model is
injective with respect to connected MELL proofstructures.