  Publications inherent to the project
[1]

Andrea Asperti, Paolo Coppola, and Simone Martini.
(Optimal) duplication is not elementary recursive.
Information and Computation, 193Issue 1:2156, 2004.
[ bib ]

[2]

Paolo Coppola and Simone Martini.
Optimizing optimal reduction: A type inference algorithm for
elementary affine logic.
ACM Trans. Comput. Logic, 7(2):219260, 2006.
[ bib ]

[3]

Ugo Dal Lago.
Semantic Frameworks for Implicit Computational Complexity.
PhD thesis, Dipartimento di Informatica, Università degli Studi di
Bologna, March 2006.
[ bib ]

[4]

Ugo Dal Lago and Simone Martini.
Phase semantics and decidability of elementary affine logic.
Theoretical Computer Science, 318(3):409433, 2004.
[ bib ]

[5]

Ugo Dal Lago and Patrick Baillot.
Light affine logic, uniform encodings and polynomial time.
Mathematical Structures in Computer Science, 2006.
Accepted for Pubblication.
[ bib ]

[6]

Ugo Dal Lago.
Context semantics, linear logic and computational complexity.
In Logic in Computer Science, 21th International Symposium,
Proceedings. IEEE Computer Society, 2006.
to appear.
[ bib ]

[7]

Ugo Dal Lago and Simone Martini.
An invariant cost model for the lambda calculus.
In Benedikt Löwe Arnold Beckmann, Ulrich Berger and John Tucker,
editors, Logical Approaches to Computational Barriers, Second Conference
on Computability in Europe, volume 3988 of Lecture Notes in Computer
Science. Springer, 2006.
to appear.
[ bib ]

[8]

Ugo Dal Lago.
The geometry of linear higherorder recursion.
In Logic in Computer Science, 20th International Symposium,
Proceedings, pages 366375. IEEE Computer Society, 2005.
[ bib ]

[9]

Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca.
Elementary affine logic and the callbyvalue lambda calculus.
In Pawel Urzyczyn, editor, Typed Lambda Calculi and
Applications, 7th International Conference, Proceedings, volume 3461 of
Lecture Notes in Computer Science, pages 131145. Springer, 2005.
[ bib ]

[10]

Ugo Dal Lago and Martin Hofmann.
Quantitative models and implicit complexity.
In R. Ramanujam and Sandeep Sen, editors, Foundations of
Software Technology and Theoretical Computer Science, Proceedings, volume
3821 of Lecture Notes in Computer Science, pages 189200. Springer,
2005.
[ bib ]

[11]

Stefano Guerrini and Andrea Masini.
Continuations, proofs and tests.
Technical Report cs.LO/0605043, Cornell University Library, 2006.
[ bib 
.pdf ]
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
way.

[12]

Stefano Baratella and Andrea Masini.
A note on unbounded metric temporal logic over dense time domains.
Technical Report RR 39/2005, Dipartimento di Informatica,
Università di Verona, Italy, 2005.
[ bib 
.pdf ]
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.

[13]

Damiano Mazza.
Linear logic & polynomial tyme.
to appear in Mathematical Structures in Computer Science, 2006.
[ bib 
.pdf ]
Light and Elementary Linear Logic, the cornerstones at
the interface between logic and implicit computational complexity, were
originally introduced by Girard as ``standalone'' 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 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.

[14]

Damiano Mazza.
Multiport interaction nets and concurrency.
In M. Abadi and L .de Alfaro, editors, Proceedings of CONCUR
2005, volume 3653 of Lecture Notes in Computer Sciences, pages 2135.
Springer, 2005.
[ bib 
.pdf ]
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 picalculus in them.
We thus obtain a faithful graphical representation of the picalculus in which every reduction step is decomposed in fully local graphrewriting rules.

[15]

Damiano Mazza.
Observational equivalence for the interaction combinators and
internal separation.
In I. Mackie, editor, Proceedings of TERMGRAPH 2006, Electronic
Notes in Theoretical Computer Science, pages 716. Elsevier, 2006.
[ bib 
.pdf ]
We define an observational equivalence for Lafont's interaction combinators,
which we prove to be the least discriminating nontrivial congruence on total nets (nets admitting a deadlockfree normal form) respecting reduction.
More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the lambdacalculus.

[16]

Claudia Faggian Paolo Di Giamberardino.
Jump from parallel to sequential proofs: multiplicatives.
In to appear in : Proceedings of Computer Science Logic 2006,
2006.
[ bib ]
We introduce a new class of multiplicative
proof nets, Jproof nets, which are a typed version of
Faggian and Maurel's multiplicative Lnets. In Jproof 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.

[17]

Michele Pagani.
Proofs, denotational semantics and observational equivalences in
multiplicative linear logic.
Mathematical Structures in Computer Science, ??(??):??, 2006.
To appear.
[ bib 
.pdf ]
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.

[18]

Michele Pagani.
Proof nets and cliques: towards the understanding of analytical
proofs.
PhD thesis, Università degli Studi di Roma and Université de la
Méditerranée (AixMarseille II), April 2006.
[ bib 
.pdf ]

[19]

Michele Pagani.
Acyclicity and coherence in multiplicative and exponential linear
logic.
Submitted, 2006.
[ bib 
.pdf ]
We give a geometric condition that
characterizes MELL proof structures whose interpretation is
a clique in nonuniform coherent spaces: visible acyclicity.
We define the 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
reduction.

[20]

Luca Paolini.
A stable programming language.
Information and Computation, 204(3):339375, 2006.
[ bib 
.pdf ]
It is wellknown that stable models
(as dIdomains, 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 PCFlike 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.

[21]

Luca Paolini, Elaine Pimentel, and Simona Ronchi Della Rocca.
An operational characterization of strong normalization.
In Luca Aceto and Anna Ingólfsdóttir, editors,
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, volume
3921 of Lecture Notes in Computer Science, pages 367381, Vienna,
Austria, March 2006. Springer.
[ bib 
.pdf ]
The paper introduces the Φcalculus,
a new callbyvalue version of λcalculus,
following the spirit of Plotkin's λβ_{v}calculus.
Such a language satisfies some properties,
in particular the set of solvable terms in it coincides with the set
of βstrongly normalizing terms in the classical λcalculus.

[22]

Simona Ronchi Della Rocca and Luca Paolini.
The Parametric λCalculus: a Metamodel for Computation.
Texts in Theoretical Computer Science: An EATCS Series.
SpringerVerlag, Berlin, 2004.
[ bib 
.html 
.html ]

[23]

Luca Paolini, Elaine Pimentel, and Simona Ronchi Della Rocca.
Lazy strong normalization.
In Proceedings of Intersection Types and Related Systems
(ITRS'04), a Satellite Workshop of the Symposium on Logic in Computer Science
(LICS'04), volume 136C of Electronic Notes in Theoretical Computer
Science, pages 103116, 2004.
[ bib 
.pdf ]
Among all the reduction strategies for the untyped
λcalculus, the so called lazy βevaluation is
of particular interest due to its large applicability to
functional programming languages (e.g. Haskell [?]). This
strategy reduces only redexes not inside a lambda abstraction.
The lazy strongly β normalizing terms are the
λterms that don't have infinite lazy βreduction
sequences.
This paper presents a logical characterization of
lazy strongly βnormalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between callbyname and callbyvalue
λcalculus.
In fact, it turns out that the class of lazy strongly
βnormalizing terms coincides with that of callbyvalue potentially
valuable terms. This last class is of particular interest since it
is a key notion for characterizing solvability in the
callbyvalue setting.

[24]

Luca Paolini and Simona Ronchi Della Rocca.
Parametric parameter passing lambdacalculus.
Information and Computation, 189(1):87106, February 2004.
[ bib 
.ps ]
A λcalculus is defined, which is parametric with respect to a set
Δ of input values and subsumes all the different λcalculi
given in the literature,
in particular the classical one and
the callbyvalue λ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 Δ and a set
Θ of output values.

[25]

Luca Paolini.
Lambdatheories: some investigations.
PhD thesis, Università degli Studi di Genova and Université de la
Méditerranée (AixMarseille II), January 2004.
[ bib 
.pdf ]
In this thesis we present somes investigations on λ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 λcalculus is defined and investigated, which is parametric with respect to a set
Δ of input values and subsumes all the different (pure and untyped) λcalculi given in the literature,
in particular the classical one and the callbyvalue λcalculus of Plotkin.
In the second part, the semantics of the parametric λΔcalculus is considered.
A universal operational semantics is given through a reduction machine,
parametric with respect to both Δ and a set Θ of output values.
Hence, a syntactical kind of model, said λΔ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.

[26]

E. Pimentel, S. Ronchi Della Rocca, and L. Roversi.
Towards a prooftheoretical justification for intersection types.
Accepted for presentation at the workshop Structures and Deduction
(SD'05), a satellite scientific event of ICALP'05., July 2005.
[ bib 
.pdf ]
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
metatheoretical 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 prooftheoretical
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 implicationconjunction
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 subformula properties as well as that
the Intersection Type assignment can be viewed as standard term
decoration of ISL.

[27]

Luigi Liquori and Simona Ronchi Della Rocca.
Intersection types a la church.
Information and Computation, To Appear, 2006.
[ bib ]

[28]

Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca.
Elementary affine logic and the call by value lambda calculus.
In Pawel Urzyczyn, editor, TLCA'05, volume 3461 of Lecture
Notes in Computer Science, pages 131145. Springer, 2005.
[ bib 
.pdf ]

[29]

Paolo Coppola and Simona Ronchi Della Rocca.
Principal typing for lambda calculus in elementary affine logic.
Fundamenta Informaticae, 65(12):87112, 2005.
[ bib 
.pdf ]

[30]

Luigi Liquori and Simona Ronchi Della Rocca.
Towards an intersection typed system a la church.
In ITRS'04, volume 136, pages 4356. Electronic Notes in
Theoretical Computer Science, 2005.
[ bib 
.pdf ]

[31]

Giulio Manzonetto and Antonino Salibra.
Boolean algebras for lambda calculus.
In Proceedings of 21st Annual IEEE Symposium on Logic in
Computer Science (LICS'06). IEEE Computer Society Publications, 2006.
[ bib 
.pdf ]
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
semantics.

[32]

Chantal Berline and Antonino Salibra.
Easiness in graph models.
Theoretical Computer Science, 354Issue 1:423, 2006.
[ bib 
.pdf ]
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 quasiidentities 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.

[33]

Stefania Lusin and Antonino Salibra.
The lattice of lambda theories.
Journal of logic and computation, 14 Issue 3:373394, 2004.
[ bib 
.pdf ]

[34]

Antonio Bucciarelli and Antonino Salibra.
The sensible graph theories of lambda calculus.
In Proceedings of 19th Annual IEEE Symposium on Logic in
Computer Science (LICS'04). IEEE Computer Society Publications, 2004.
[ bib 
.pdf ]
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 nonexistence of a graph model whose equational
theory is exactly the minimal lambda theory lambdabeta.

[35]

Olivier Laurent and Lorenzo Tortora de Falco.
Slicing polarized additive normalization.
In Thomas Ehrhard, JeanYves Girard, Paul Ruet, and Philip Scott,
editors, Linear Logic in Computer Science, volume 316 of London
Mathematical Society Lecture Note Series, pages 247282. Cambridge
University Press, 2004.
[ bib ]

[36]

Olivier Laurent, Myriam Quatrini, and Lorenzo Tortora de Falco.
Polarized and focalized linear and classical proofs.
Annals of Pure and Applied Logic, 134, Issues 23:95316,
2005.
[ bib ]

[37]

Olivier Laurent and Lorenzo Tortora de Falco.
Obsessional cliques: a semantic characterization of bounded time
complexity.
In Proceedings of the twentyfirst annual IEEE symposium on
Logic In Computer Science (LICS '06), 2006.
[ bib ]

This file has been generated by
bibtex2html 1.75
