Publications inherent to the project

[1] Andrea Asperti, Paolo Coppola, and Simone Martini. (Optimal) duplication is not elementary recursive. Information and Computation, 193Issue 1:21-56, 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):219-260, 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):409-433, 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 higher-order recursion. In Logic in Computer Science, 20th International Symposium, Proceedings, pages 366-375. IEEE Computer Society, 2005.
[ bib ]
[9] Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca. Elementary affine logic and the call-by-value lambda calculus. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications, 7th International Conference, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 131-145. 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 189-200. 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 ``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 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 21-35. 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 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.
[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 7-16. Elsevier, 2006.
[ bib | .pdf ]
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öhm's Theorem for the lambda-calculus.
[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, 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.
[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 (Aix-Marseille 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 non-uniform 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):339-375, 2006.
[ bib | .pdf ]
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.
[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 367-381, Vienna, Austria, March 2006. Springer.
[ bib | .pdf ]
The paper introduces the Φ-calculus, a new call-by-value 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. Springer-Verlag, 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 103-116, 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 call-by-name and call-by-value λ-calculus.
In fact, it turns out that the class of lazy strongly β-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.
[24] Luca Paolini and Simona Ronchi Della Rocca. Parametric parameter passing lambda-calculus. Information and Computation, 189(1):87-106, 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 call-by-value λ-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. Lambda-theories: some investigations. PhD thesis, Università degli Studi di Genova and Université de la Méditerranée (Aix-Marseille 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 call-by-value λ-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 proof-theoretical 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 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.
[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 131-145. Springer, 2005.
[ bib | .pdf ]
[29] Paolo Coppola and Simona Ronchi Della Rocca. Principal typing for lambda calculus in elementary affine logic. Fundamenta Informaticae, 65(1-2):87-112, 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 43-56. 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:4-23, 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 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.
[33] Stefania Lusin and Antonino Salibra. The lattice of lambda theories. Journal of logic and computation, 14 Issue 3:373-394, 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 non-existence of a graph model whose equational theory is exactly the minimal lambda theory lambda-beta.
[35] Olivier Laurent and Lorenzo Tortora de Falco. Slicing polarized additive normalization. In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip Scott, editors, Linear Logic in Computer Science, volume 316 of London Mathematical Society Lecture Note Series, pages 247-282. 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 2-3:95-316, 2005.
[ bib ]
[37] Olivier Laurent and Lorenzo Tortora de Falco. Obsessional cliques: a semantic characterization of bounded time complexity. In Proceedings of the twenty-first annual IEEE symposium on Logic In Computer Science (LICS '06), 2006.
[ bib ]

This file has been generated by bibtex2html 1.75