@ARTICLE{Asperti+Coppola+Martini:iandc2004, 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} }

@ARTICLE{Coppola+Martini:tocl2006, 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 = {http://doi.acm.org/10.1145/1131313.1131315}, PUBLISHER = {ACM Press}, ADDRESS = {New York, NY, USA} }

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

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

@ARTICLE{MSCS2006, 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.} }

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

@INPROCEEDINGS{CIE2006, 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} }

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

@INPROCEEDINGS{TLCA2005, 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 Calculus.}, 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} }

@INPROCEEDINGS{FSTTCS2005, 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} }

@TECHREPORT{GueMas-06, 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 way.}, 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 = {http://www.di.univr.it/documenti//RapportoRicercaEst/allegato/allegato484828.pdf}, YEAR = {2006} }

@TECHREPORT{BarMas-05, 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, Italy}, NUMBER = {RR 39/2005}, TITLE = {A note on unbounded Metric Temporal Logic over dense time domains}, URL = {http://www.di.univr.it/documenti//RapportoRicerca/allegato/allegato922543.pdf}, YEAR = {2005} }

@ARTICLE{Mazza:LLandPTime, AUTHOR = {Damiano Mazza}, TITLE = {Linear Logic \& Polynomial Tyme}, JOURNAL = {to appear in Mathematical Structures in Computer Science}, YEAR = 2006, PDF = {http://iml.univ-mrs.fr/~mazza/papers/LLandPTime-MSCS.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.} }

@INPROCEEDINGS{Mazza:mINS, 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 L~.de 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 = {http://iml.univ-mrs.fr/~mazza/papers/mINSAndConcurrency-CONCUR05.pdf} }

@INPROCEEDINGS{Mazza:CombSep, 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 = {http://iml.univ-mrs.fr/~mazza/papers/CombSep-TERMGRAPH06.pdf} }

@INPROCEEDINGS{DgFjump, 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.} }

@ARTICLE{pagani06mscs, 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 = {http://logica.uniroma3.it/~pagani/sepMLL.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.} }

@PHDTHESIS{pagani06phd, AUTHOR = {Michele Pagani}, TITLE = {Proof nets and cliques: towards the understanding of analytical proofs}, MONTH = APR, SCHOOL = {Universit\`a degli Studi di Roma and Universit\'e de la M\'editerran\'ee (Aix-Marseille {II})}, YEAR = 2006, PDF = {http://logica.uniroma3.it/~pagani/tesi.pdf} }

@UNPUBLISHED{pagani06unp, AUTHOR = {Michele Pagani}, TITLE = {Acyclicity and Coherence in Multiplicative and Exponential Linear Logic}, NOTE = {Submitted}, YEAR = 2006, PDF = {http://logica.uniroma3.it/~pagani/vacCSL.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 reduction.} }

@ARTICLE{paolini05iandc, AUTHOR = {Paolini, Luca}, TITLE = {A Stable Programming Language}, PAGES = {339-375}, VOLUME = {204}, NUMBER = {3}, JOURNAL = {Information and Computation}, YEAR = 2006, PDF = {http://www.di.unito.it/~paolini/papers/stpcf.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.} }

@INPROCEEDINGS{paolini05fossacs, 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 = {http://www.di.unito.it/~paolini/papers/bsn.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.} }

@BOOK{ronchi04book, AUTHOR = {Ronchi Della Rocca, Simona and Paolini, Luca}, TITLE = {The Parametric $\lambda$-Calculus: a Metamodel for Computation}, PUBLISHER = {Springer-Verlag}, SERIES = {Texts in Theoretical Computer Science: An EATCS Series}, PAGES = 252, ADDRESS = {Berlin}, YEAR = 2004, URL = {http://www.springer.com/sgw/cda/frontpage/0,,5-40356-72-14202886-0,00.html}, PDF = {http://www.di.unito.it/~paolini/BookParametric.html}, TAG = {Springer-Verlag} }

@INPROCEEDINGS{paolini04itrs, 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 = {http://www.di.unito.it/~ronchi/papers/lsn.pdf}, LOCALFILE = {http://www.di.unito.it/~paolini/papers/lsn05.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 sequences.\\ 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 $\lambda$-calculus.\\ 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.} }

@ARTICLE{paolini04iandc, 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}, MONTH = FEB, PUBLISHER = {Elsevier}, PDF = {http://www.di.unito.it/~ronchi/papers/cr.ps}, LOCALFILE = {http://www.di.unito.it/~paolini/papers/ppp04.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. } }

@PHDTHESIS{paolini04phd, AUTHOR = {Luca Paolini}, TITLE = {Lambda-theories: some investigations}, MONTH = JAN, SCHOOL = {Universit\`a degli Studi di Genova and Universit\'e de la M\'editerran\'ee (Aix-Marseille {II})}, YEAR = 2004, PDF = {http://www.di.unito.it/~paolini/papers/phd.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.} }

@UNPUBLISHED{Pimentel+Ronchi+Roversi:2004, AUTHOR = {Pimentel, E. and Ronchi Della Rocca, S. and Roversi, L.}, TITLE = {Towards a proof-theoretical justification for Intersection Types}, MONTH = {July}, YEAR = {2005}, URL = {http://www.di.unito.it/~ronchi/papers/ISL.pdf}, 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.} }

@ARTICLE{liquori06iandc, 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 }

@INPROCEEDINGS{Cop-DLag-Ron:EALCBV-04, AUTHOR = {Paolo Coppola and Dal Lago, Ugo and Ronchi Della Rocca, Simona}, TITLE = {Elementary Affine Logic and the Call by Value Lambda Calculus }, PDF = {http://www.di.unito.it/~ronchi/papers/llcbv.pdf}, YEAR = 2005, PAGES = {131-145}, EDITOR = {Pawel Urzyczyn}, BOOKTITLE = {TLCA'05}, TAG = {TLCA'05}, PUBLISHER = {Springer}, SERIES = {Lecture Notes in Computer Science}, VOLUME = 3461 }

@ARTICLE{Cop+Ron:FI-2005, 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 = {http://www.dimi.uniud.it/~coppola/papers/EA-typing.pdf} }

@INPROCEEDINGS{Liqu-Ronc:ENTCS04, AUTHOR = {Liquori, Luigi and Ronchi Della Rocca, Simona}, TITLE = {Towards an Intersection Typed System a la Church}, BOOKTITLE = {ITRS'04}, TAG = {ITRS'04}, PUBLISHER = {Electronic Notes in Theoretical Computer Science}, VOLUME = {136}, PAGES = {43-56}, PDF = {http://www.di.unito.it/~ronchi/papers/itrs-liquori-ronchi.pdf}, YEAR = 2005 }

@INPROCEEDINGS{Manzonetto+Salibra:Lics2006, 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 semantics.}, PDF = {http://www.dsi.unive.it/~salibra/LICS2006pubblicata.pdf} }

@ARTICLE{Berline+Salibra:tcs2006, 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 = {http://www.dsi.unive.it/~salibra/TrueHome/Papers/chantalnino24Jan05.pdf} }

@ARTICLE{Lusin+Salibra:jlc2004, 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 = {http://www.dsi.unive.it/~salibra/TrueHome/Papers/JLC02-35-lusin-salibra.pdf} }

@INPROCEEDINGS{Bucciarelli+Salibra:Lics2004, 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 = {http://www.dsi.unive.it/~salibra/TrueHome/Papers/LICS2004.pdf} }

@INPROCEEDINGS{slice, 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} }

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

@INPROCEEDINGS{lics06, 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 symposium on Logic In Computer Science (LICS '06)}, YEAR = {2006} }

*This file has been generated by
bibtex2html 1.75*