AUTHOR = {Andrea Asperti and Paolo Coppola and Simone Martini},
  JOURNAL = {Information and Computation},
  PAGES = {21--56},
  TITLE = {({O}ptimal) duplication is not elementary recursive},
  VOLUME = {193Issue 1},
  YEAR = {2004}

  AUTHOR = {Paolo Coppola and Simone Martini},
  TITLE = {Optimizing optimal reduction: A type inference algorithm  
for elementary affine logic},
  JOURNAL = {ACM Trans. Comput. Logic},
  VOLUME = {7},
  NUMBER = {2},
  YEAR = {2006},
  ISSN = {1529-3785},
  PAGES = {219--260},
  DOI = {},
  PUBLISHER = {ACM Press},
  ADDRESS = {New York, NY, USA}

  AUTHOR = {Dal Lago, Ugo},
  TITLE = {Semantic Frameworks for Implicit Computational Complexity},
  SCHOOL = {Dipartimento di Informatica, Universit\`a degli Studi di
  YEAR = {2006},
  MONTH = {March}

  AUTHOR = {Dal Lago, Ugo and Martini, Simone},
  TITLE = {Phase Semantics and Decidability of Elementary Affine
  JOURNAL = {Theoretical Computer Science},
  YEAR = {2004},
  VOLUME = {318},
  NUMBER = {3},
  PAGES = {409--433}

  AUTHOR = {Dal Lago, Ugo and Baillot, Patrick},
  TITLE = {Light Affine Logic, Uniform Encodings and Polynomial Time},
  JOURNAL = {Mathematical Structures in Computer Science},
  YEAR = {2006},
  NOTE = {Accepted for Pubblication.}

  AUTHOR = {Dal Lago, Ugo},
  TITLE = {Context Semantics, Linear Logic and Computational
  BOOKTITLE = {Logic in Computer Science, 21th International Symposium,
  YEAR = {2006},
  PUBLISHER = {IEEE Computer Society},
  NOTE = {to appear}

  EDITOR = {Arnold Beckmann, Ulrich Berger, Benedikt L\"owe and
John Tucker},
  AUTHOR = {Dal Lago, Ugo and Martini, Simone},
  TITLE = {An Invariant Cost Model for the Lambda Calculus},
  BOOKTITLE = {Logical Approaches to Computational Barriers, Second
Conference on Computability in Europe},
  YEAR = {2006},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = {3988},
  NOTE = {to appear}

  AUTHOR = {Dal Lago, Ugo},
  TITLE = {The Geometry of Linear Higher-Order Recursion},
  BOOKTITLE = {Logic in Computer Science, 20th International Symposium,
  YEAR = {2005},
  PAGES = {366-375},
  PUBLISHER = {IEEE Computer Society}

  EDITOR = {Pawel Urzyczyn},
  AUTHOR = {Coppola, Paolo and
               Dal Lago,Ugo and
               Ronchi Della Rocca, Simona},
  TITLE = {Elementary Affine Logic and the Call-by-Value Lambda
  BOOKTITLE = {Typed Lambda Calculi and Applications, 7th International
Conference, Proceedings},
  YEAR = {2005},
  PAGES = {131-145},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = {3461}

  EDITOR = {Ramanujam, R. and Sen, Sandeep},
  AUTHOR = {Dal Lago, Ugo and Hofmann, Martin},
  TITLE = {Quantitative Models and Implicit Complexity},
  BOOKTITLE = {Foundations of Software Technology and Theoretical
Computer Science, Proceedings},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3821},
  YEAR = {2005},
  PAGES = {189--200}

  ABSTRACT = {Continuation Passing Style (CPS) is one of the
                 most important issues in the field of functional
                 programming languages, and the quest for a primitive
                 notion of types for continuation is still
                 open. Starting from the notion of ``test'' proposed
                 by Girard, we develop a notion of test for
                 intuitionistic logic. We give a complete deductive
                 system for tests and we show that it is good to deal
                 with ``continuations''. In particular, in the
                 proposed system it is possible to work with Call by
                 Value and Call by Name translations in a uniform
  AUTHOR = {Guerrini, Stefano and Masini, Andrea},
  DATE-ADDED = {2006-06-19 11:18:56 +0200},
  DATE-MODIFIED = {2006-06-19 11:22:35 +0200},
  INSTITUTION = {Cornell University Library},
  NUMBER = {cs.LO/0605043},
  TITLE = {Continuations, proofs and tests},
  URL = {},
  YEAR = {2006}

  ABSTRACT = {We investigate the consequences of removing the
                 infinitary axiom and rules from a previously defined
                 proof system for a fragment of propositional metric
                 temporal logic over dense time.},
  AUTHOR = {Baratella, Stefano and Masini, Andrea},
  DATE-ADDED = {2006-06-19 11:11:37 +0200},
  DATE-MODIFIED = {2006-06-19 11:19:34 +0200},
  INSTITUTION = {Dipartimento di Informatica, Universit\`a di Verona, 
  NUMBER = {RR 39/2005},
  TITLE = {A note on unbounded Metric Temporal Logic over dense time 
  URL = {},
  YEAR = {2005}

  AUTHOR = {Damiano Mazza},
  TITLE = {Linear Logic \& Polynomial Tyme},
  JOURNAL = {to appear in Mathematical Structures in Computer Science},
  YEAR = 2006,
  PDF = {},
  ABSTRACT = {Light and Elementary Linear Logic, the cornerstones at 
the interface between logic and implicit computational complexity, were 
originally introduced by Girard as ``stand-alone'' logical systems with 
a (somewhat awkward) sequent calculus of their own. The latter has later 
been reformulated by Danos and Joinet as a proper subsystem of linear 
logic, whose proofs satisfy a certain structural condition. We extend 
this approach to polytime computation, finding two solutions: the first 
one, obtained by a simple extension of Danos\&Joinet's condition, 
closely resembles Asperti's Light Affine Logic and enjoys \emph{polystep 
strong normalization} (the polynomial bound does not depend on the 
reduction strategy); the second one, which needs more complex 
conditions, exactly corresponds to Girard's Light Linear Logic.}

  AUTHOR = {Damiano Mazza},
  TITLE = {Multiport Interaction Nets and Concurrency},
  BOOKTITLE = {Proceedings of CONCUR 2005},
  SERIES = {Lecture Notes in Computer Sciences},
  PUBLISHER = {Springer},
  EDITOR = {M.~Abadi and Alfaro},
  VOLUME = {3653},
  PAGES = {21--35},
  YEAR = {2005},
  ABSTRACT = {We consider an extension of Lafont's Interaction Nets, called Multiport Interaction Nets, 
and show that they are a model of concurrent computation by encoding the full pi-calculus in them. 
We thus obtain a faithful graphical representation of the pi-calculus in which every reduction step is decomposed in fully local graph-rewriting rules.},
  PDF = {}

  AUTHOR = {Damiano Mazza},
  TITLE = {Observational Equivalence for the Interaction Combinators and Internal Separation},
  BOOKTITLE = {Proceedings of TERMGRAPH 2006},
  SERIES = {Electronic Notes in Theoretical Computer Science},
  PUBLISHER = {Elsevier},
  EDITOR = {I.~Mackie},
  PAGES = {7--16},
  YEAR = {2006},
  ABSTRACT = {We define an observational equivalence for Lafont's interaction combinators, 
which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. 
More interestingly, this equivalence enjoys an internal separation property similar to that of B\"ohm's Theorem for the lambda-calculus.},
  PDF = {}

  AUTHOR = {Paolo Di Giamberardino, Claudia Faggian},
  TITLE = {Jump from parallel to sequential proofs: multiplicatives},
  BOOKTITLE = {to appear in : Proceedings of Computer
Science Logic 2006},
  YEAR = {2006},
  ABSTRACT = {We introduce a new class of multiplicative
proof nets, J-proof nets, which are a typed version of
Faggian and Maurel's multiplicative L-nets. In J-proof nets,
by gradual insertion of sequentiality constraints, we can
characterize nets with different degrees of sequentiality;
as a byproduct, we obtain a simple proof of the
sequentialisation theorem.}

  AUTHOR = {Pagani, Michele},
  TITLE = {Proofs, Denotational Semantics and Observational
Equivalences in Multiplicative Linear Logic},
  PAGES = {??},
  VOLUME = {??},
  NUMBER = {??},
  NOTE = {To appear.},
  JOURNAL = {Mathematical Structures in Computer Science},
  YEAR = 2006,
  PDF = {},
  ABSTRACT = {We study full completeness and syntactical
separability of MLL proof nets with the mix rule. The
general method we use consists first in addressing the two
questions in the less restrictive framework of proof
structures, and then in adapting the results to proof nets.\\
At the level of proof structures, we find a semantical
characterization of their interpretations in relational
semantics, and we define an observational equivalence which
is proved to be the equivalence induced by cut elimination.
Hence, we obtain a semantical characterization (in coherent
spaces) and an observational equivalence for the proof nets
with the mix rule.}

  AUTHOR = {Michele Pagani},
  TITLE = {Proof nets and cliques: towards the understanding
of analytical proofs},
  SCHOOL = {Universit\`a degli Studi di Roma and
Universit\'e de la
            M\'editerran\'ee (Aix-Marseille {II})},
  YEAR = 2006,
  PDF = {}

  AUTHOR = {Michele Pagani},
  TITLE = {Acyclicity and Coherence in Multiplicative and
Exponential Linear Logic},
  NOTE = {Submitted},
  YEAR = 2006,
  PDF = {},
  ABSTRACT = {We give a geometric condition that
characterizes MELL proof structures whose interpretation is
a clique in non-uniform coherent spaces: visible acyclicity.\\

We define the \emph{visible paths} and we prove that the
proof structures which have no visible cycles are exactly
those whose interpretation is a clique.\\

It turns out that visible acyclicity has also nice
computational properties, especially it is stable under cut

  AUTHOR = {Paolini, Luca},
  TITLE = {A Stable Programming Language},
  PAGES = {339-375},
  VOLUME = {204},
  NUMBER = {3},
  JOURNAL = {Information and Computation},
  YEAR = 2006,
  PDF = {},
  TAG = {Information and Computation},
  ABSTRACT = {It is well-known that stable models 
(as dI-domains, qualitative domains and coherence spaces) 
are not fully abstract for the language $PCF$.
This fact is related to the existence of stable parallel functions
and of stable functions that are not monotone with respect to the extensional order, 
which  cannot be defined by programs of $PCF$.\\
In this paper, a paradigmatic programming language named $StPCF$
is proposed, which extends the language $PCF$ with two additional operators.
The operational description of the extended language is presented in an effective way, 
although the evaluation of one of the new operators cannot be
formalized in a PCF-like rewrite system.\\
Since $StPCF$ can define all finite cliques of coherence spaces
the above gap with stable models is filled,
consequently stable models are fully abstract for the extended language.}

  AUTHOR = {Paolini, Luca and Pimentel, Elaine and Ronchi Della Rocca, Simona},
  TITLE = {An Operational Characterization of Strong Normalization},
  BOOKTITLE = {Proceedings of  9th International Conference on
Foundations of Software Science and Computation Structures -- FOSSACS 2006,
Held as Part of the
European Joint Conferences on Theory and Practice of Software 2006},
  EDITOR = {Luca Aceto and
               Anna Ing{\'o}lfsd{\'o}ttir},
  ADDRESS = {Vienna, Austria},
  MONTH = {March},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3921},
  PAGES = {367-381},
  YEAR = {2006},
  ISBN = {3-540-33045-3},
  PDF = {},
  TAG = {FOSSACS 2006},
  ABSTRACT = {The paper introduces the $\Phi$-calculus,
a new call-by-value version of  $\lambda$-calculus,
following the spirit of Plotkin's $\lambda\beta_{v}$-calculus.
Such a language satisfies some properties,
in particular the set of solvable terms in it  coincides with the set
of $\beta$-strongly normalizing terms in the classical $\lambda$-calculus.}

  AUTHOR = {Ronchi Della Rocca, Simona and Paolini, Luca},
  TITLE = {The Parametric $\lambda$-Calculus: a Metamodel for
  PUBLISHER = {Springer-Verlag},
  SERIES = {Texts in Theoretical Computer Science:
                An EATCS Series},
  PAGES = 252,
  ADDRESS = {Berlin},
  YEAR = 2004,
  URL = {,,5-40356-72-14202886-0,00.html},
  PDF = {},
  TAG = {Springer-Verlag}

  AUTHOR = {Paolini, Luca and Pimentel, Elaine and Ronchi Della Rocca, Simona},
  TITLE = {Lazy strong normalization},
  BOOKTITLE = {Proceedings of Intersection Types and Related Systems (ITRS'04),
a Satellite Workshop of the Symposium on Logic in Computer Science (LICS'04)},
  SERIES = {Electronic Notes in Theoretical Computer Science},
  PAGES = {103-116},
  VOLUME = {136C},
  PDF = {},
  TAG = {Intersection Types and Related Systems 2004},
  YEAR = 2004,
  ABSTRACT = {Among all the reduction strategies for the untyped
$\lambda$-calculus, the so called {\em lazy $\beta$-evaluation} is
of particular interest due to its large applicability to
functional programming languages (e.g. Haskell~\cite{Bi98}). This
strategy reduces only redexes not inside a lambda abstraction.\\
The lazy strongly $\beta$- normalizing terms are the
$\lambda$-terms that don't have infinite lazy $\beta$-reduction
This paper presents a logical characterization of
lazy strongly $\beta$-normalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between call-by-name and call-by-value
In fact, it turns out that the class of lazy strongly
$\beta$-normalizing terms coincides with that of call-by-value potentially
valuable terms. This last class is of particular interest since it
is a key notion for characterizing solvability in the
call-by-value setting.}

  AUTHOR = {Paolini, Luca and Ronchi Della Rocca, Simona},
  TITLE = {Parametric parameter passing lambda-calculus},
  JOURNAL = {Information and Computation},
  VOLUME = {189},
  NUMBER = {1},
  PAGES = {87-106},
  PUBLISHER = {Elsevier},
  PDF = {},
  TAG = {Information and Computation},
  YEAR = 2004,
  ABSTRACT = {A $\lambda$-calculus is defined, which is parametric with respect to a set 
$\Delta$ of input values and subsumes all the different $\lambda$-calculi 
given in the literature, 
in particular the classical one and 
the call-by-value $\lambda$-calculus of Plotkin. 
It is proved that it enjoy the confluence property, and a necessary and 
sufficient condition
is given, under which it enjoys the standardization property. Its operational 
semantics is given
through a reduction machine, parametric with respect to both $\Delta$ and a set 
$\Theta$ of output values. }

  AUTHOR = {Luca Paolini},
  TITLE = {Lambda-theories: some investigations},
  SCHOOL = {Universit\`a degli Studi di Genova and Universit\'e de la
            M\'editerran\'ee (Aix-Marseille {II})},
  YEAR = 2004,
  PDF = {},
  TAG = {Universit\`a degli Studi di Genova and Universit\'e de la
            M\'editerran\'ee (Aix-Marseille {II})},
  ABSTRACT = {In this thesis we present somes investigations on $\lambda$-calculi, both untyped and typed. 
The first two parts concerning some pure untyped calculi, 
while the last concerns $PCF$ and an extension of its syntax.\\
In the first part, a $\lambda$-calculus is defined and investigated, which is parametric with respect to a set 
$\Delta$ of input values and subsumes all the different (pure and untyped)  $\lambda$-calculi  given in the literature,  
in particular the classical one and the call-by-value $\lambda$-calculus of Plotkin. 
In the second part, the semantics of the parametric $\lambda\Delta$-calculus is considered.\\
A universal operational semantics is given through a reduction machine, 
parametric with respect to both $\Delta$ and a set $\Theta$ of output values. 
Hence, a  syntactical kind of model, said $\lambda\Delta$-interaction model is defined
and showed to be fully abstract for the main interesting universal operational semantics.
The last part of the thesis  concerns an investigation of a programming language extending $PCF$ 
by some stable operators, in the sense of Berry. 
The new language is fully abstract with respect to stable domains.}

  AUTHOR = {Pimentel, E. and Ronchi Della Rocca, S. and Roversi, L.},
  TITLE = {Towards a proof-theoretical justification for Intersection 
  MONTH = {July},
  YEAR = {2005},
  URL = {},
  ABSTRACT = {It is well known that derivations in 
  Intersection Types (IT) form
  a strict subset of deductions in Intuitionistic Logic (LJ) -- up
  to term decorations -- in the sense that IT imposes a
  meta-theoretical restriction on proofs: conjunction can be
  introduced only between derivations that are synchronized with
  respect to the implication.
  The goal of this work is to present a proof-theoretical
  justification for IT. In particular, we discuss the relationship
  between the intersection connective and the intuitionistic
  conjunction. For this purpose, we define a new logical system
  called Intersection Synchronous Logic (ISL), that proves
  properties of sets of deductions of the implication-conjunction
  fragment of LJ.
  The main idea behind ISL is the decomposition of the
  intuitionistic conjunction into two connectives, one with
  synchronous and the other with asynchronous behavior.
  Also in the present work, we prove that ISL enjoys both the
  strong normalization and sub-formula properties as well as that
  the Intersection Type assignment can be viewed as standard term
  decoration of ISL.},
  NOTE = {Accepted for presentation at the workshop Structures and Deduction
  (SD'05), a satellite scientific event of ICALP'05.}

  AUTHOR = {Liquori, Luigi and Ronchi Della Rocca, Simona},
  TITLE = {Intersection Types a la Church},
  JOURNAL = {Information and Computation},
  TAG = {Information and Computation},
  VOLUME = {To Appear},
  PAGES = {},
  YEAR = 2006

  AUTHOR = {Paolo Coppola and  Dal Lago, Ugo and Ronchi Della Rocca, Simona},
  TITLE = {Elementary Affine Logic and the Call by Value Lambda Calculus },
  PDF = {},
  YEAR = 2005,
  PAGES = {131-145},
  EDITOR = {Pawel Urzyczyn},
  TAG = {TLCA'05},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3461

  AUTHOR = {Paolo Coppola  and Ronchi Della Rocca, Simona},
  TITLE = {Principal Typing for Lambda Calculus in Elementary Affine Logic},
  JOURNAL = {Fundamenta Informaticae},
  TAG = {Fundamenta Informaticae},
  YEAR = 2005,
  VOLUME = 65,
  NUMBER = {1-2},
  PAGES = {87-112},
  PDF = {}

  AUTHOR = {Liquori, Luigi and Ronchi Della Rocca, Simona},
  TITLE = {Towards an Intersection Typed System a la Church},
  TAG = {ITRS'04},
  PUBLISHER = {Electronic Notes in Theoretical Computer Science},
  VOLUME = {136},
  PAGES = {43-56},
  PDF = {},
  YEAR = 2005

  AUTHOR = {Giulio Manzonetto and Antonino Salibra},
  TITLE = {Boolean algebras for lambda calculus},
  BOOKTITLE = {Proceedings of 21st Annual IEEE Symposium on Logic in 
Computer Science (LICS'06)},
  PUBLISHER = {IEEE Computer Society Publications},
  YEAR = {2006},
  ABSTRACT = {In this paper we show that the Stone representation theorem
for Boolean algebras can be generalized to combinatory
algebras. In every combinatory algebra there is a
Boolean algebra of central elements (playing the role of
idempotent elements in rings), whose operations are defined
by suitable combinators. Central elements are used to represent
any combinatory algebra as a Boolean product of
directly indecomposable combinatory algebras (i.e., algebras
which cannot be decomposed as the Cartesian product
of two other nontrivial algebras). Central elements are
also used to provide applications of the representation theorem
to lambda calculus. We show that the indecomposable
semantics (i.e., the semantics of lambda calculus given in
terms of models of lambda calculus, which are directly indecomposable
as combinatory algebras) includes the continuous,
stable and strongly stable semantics, and the term
models of all semisensible lambda theories. In one of the
main results of the paper we show that the indecomposable
semantics is equationally incomplete, and this incompleteness
is as wide as possible: for every recursively enumerable
lambda theory T , there is a continuum of lambda theories
including T which are omitted by the indecomposable
  PDF = {}

  AUTHOR = {Chantal Berline and Antonino Salibra},
  JOURNAL = {Theoretical Computer Science},
  PAGES = {4--23},
  TITLE = {Easiness in graph models},
  VOLUME = {354Issue 1},
  YEAR = {2006},
  ABSTRACT = {Lambda theories are equational extensions of the untyped 
lambda calculus that are closed
under derivation. The set of lambda theories is naturally equipped with a 
structure of
complete lattice, where the meet of a family of lambda theories is their 
intersection, and
the join is the least lambda theory containing their union. In this paper 
we study the
structure of the lattice of lambda theories by universal algebraic 
methods. We show that
nontrivial quasi-identities in the language of lattices hold in the 
lattice of lambda theories,
while every nontrivial lattice identity fails in the lattice of lambda 
theories if the language
of lambda calculus is enriched by a suitable finite number of constants. 
We also show that
there exists a sublattice of the lattice of lambda theories which 
satisfies: (i) a restricted form
of distributivity, called meet semidistributivity; and (ii) a nontrivial 
identity in the language
of lattices enriched by the relative product of binary relations.},
  PDF = {}

  AUTHOR = {Stefania Lusin and Antonino Salibra},
  JOURNAL = {Journal of logic and computation},
  PAGES = {373--394},
  TITLE = {The lattice of lambda theories},
  VOLUME = {14 Issue 3},
  YEAR = {2004},
  PDF = {}

  AUTHOR = {Antonio Bucciarelli and Antonino Salibra},
  TITLE = {The sensible graph theories of lambda calculus},
  BOOKTITLE = {Proceedings of 19th Annual IEEE Symposium on Logic in 
Computer Science (LICS'04)},
  PUBLISHER = {IEEE Computer Society Publications},
  YEAR = {2004},
  ABSTRACT = {A longstanding open
problem in lambda calculus is whether there exists a nonsyntactic
model whose equational theory is the least sensible
lambda theory H (generated by equating all the unsolvable
terms). A related question is whether, given a class of models,
there exist a minimal and maximal sensible lambda theory
represented by it. In this paper we give a positive answer to
this question for the semantics of lambda calculus given in
terms of graph models. We conjecture that the least sensible
graph theory, where graph theory means lambda theory of a
graph model, is equal to H, while in the main result of the
paper we characterize the greatest sensible graph theory
as the lambda theory B generated by equating terms with the
same Bohm tree. This result is a consequence of the fact that
all the equations between solvable terms, which have different
Bohm trees, fail in every sensible graph model. Further
results of the paper are: (i) the existence of a continuum
of different sensible graph theories strictly included in
B; (ii) the non-existence of a graph model whose equational
theory is exactly the minimal lambda theory lambda-beta.},
  PDF = {}

  AUTHOR = {Olivier Laurent and Tortora de Falco, Lorenzo},
  TITLE = {Slicing polarized additive normalization},
  PAGES = {247--282},
  BOOKTITLE = {Linear Logic in Computer Science},
  EDITOR = {Thomas Ehrhard and Jean-Yves Girard and Paul
Ruet and Philip Scott},
  SERIES = {London Mathematical Society Lecture Note Series},
  VOLUME = 316,
  PUBLISHER = {Cambridge University Press},
  YEAR = {2004}

  AUTHOR = {Olivier Laurent and Myriam Quatrini and Tortora
de Falco, Lorenzo},
  TITLE = {Polarized and Focalized Linear and Classical
  JOURNAL = {Annals of Pure and Applied Logic},
  VOLUME = {134, Issues 2-3},
  PAGES = {95--316},
  YEAR = {2005}

  AUTHOR = {Olivier Laurent and Tortora de Falco, Lorenzo},
  TITLE = {Obsessional cliques: a semantic
characterization of bounded time complexity},
  BOOKTITLE = {Proceedings of the twenty-first annual IEEE
on Logic In Computer Science (LICS '06)},
  YEAR = {2006}

This file has been generated by bibtex2html 1.75