AUTHOR = {Alessi, Fabio and Barbanera, Franco and
                   Dezani-Ciancaglini, Mariangiola},
  TITLE = {Intersection Types and Computational Rules},
  EDITOR = {de Queiroz, Ruy and Pimentel, Elaine and Figueiredo,
  NUMBER = {84},
  SERIES = {El. Notes in Theoret. Comput. Sci.},
  PAGES = {},
  ADDRESS = {},
  PUBLISHER = {Elsevier},
  ABSTRACT = {The invariance of the meaning of a lambda term under
                   reduction/expansion w.r.t. the considered computational
                   rules is one the minimal requirements for a lambda
                   model. Being the intersection type systems a general
                   framework for the study of semantic domains for the
                   lambda calculus, the present paper provides a
                   characterisation of "meaning invariance" in terms of
                   characterisation results for intersection types systems
                   enabling typing invariance of terms w.r.t. various
                   notions of reduction/expansion, like beta, eta and a
                   number of relevant restrictions of theirs. },
  URL = {},
  YEAR = 2003

  AUTHOR = {Andreoli, J.M. and Maieli, R. and Ruet, P.},
  TITLE = {Constraint-based proof construction in non commutative
  JOURNAL = {Theoretical Computer Science},
  NOTE = {To appear},
  YEAR = 2004

  AUTHOR = {Baillot, P. and Pedicini, M.},
  TITLE = {An embedding of {Blum-Shub-Smale} model of computation
                   in {LLL}},
  NOTE = {in preparation}

  AUTHOR = {Baillot, Patrick and Pedicini, Marco},
  TITLE = {Elementary complexity and geometry of interaction},
  JOURNAL = {Fund. Inform.},
  VOLUME = {45},
  NUMBER = {1-2},
  PAGES = {1--31},
  NOTE = {Typed lambda calculi and applications (L'Aquila, 1999)},
  ABSTRACT = { We introduce a geometry of interaction model given by
                   an algebra of clauses equipped with resolution
                   (following cite{Girard95d}) into which proofs of
                   Elementary Linear Logic can be interpreted. In order to
                   extend geometry of interaction computation (the so
                   called {\em execution formula}) to a wider class of
                   programs in the algebra than just those coming from
                   proofs, we define a variant of execution (called {\em
                   weak execution}). Its application to any program of
                   clauses is shown to terminate with a bound on the
                   number of steps which is elementary in the size of the
                   program. We establish that weak execution coincides
                   with standard execution on programs coming from proofs.},
  FJOURNAL = {Fundamenta Informaticae},
  ISSN = {0169-2968},
  MRCLASS = {03F52 (68N18 68Q55)},
  MRNUMBER = {2002j:03070},
  MRREVIEWER = {Gianfranco Mascari},
  URL = {},
  YEAR = 2001

  AUTHOR = {Ballario, P. and Pedicini, M.},
  TITLE = {Quantitative operational semantics in formal molecular
  NOTE = {in preparation}

  AUTHOR = {Baratella, S. and Masini, A.},
  TITLE = {An approach to infinitary temporal proof theory},
  JOURNAL = {Archive for Mathematical Logic},
  ABSTRACT = {Aim of this work is to investigate from a
                   proof-theoretic viewpoint a propositional and a
                   predicate sequent calculus with an omega-type schema of
                   inference that naturally interpret the propositional
                   and the predicate until--free fragments of Linear Time
                   Logic LTL respectively. The two calculi are based on a
                   natural extension of ordinary sequents and of standard
                   modal rules. We examine the pure propositional case (no
                   extralogical axioms), the propositional and the first
                   order predicate cases (both with a possibly infinite
                   set of extralogical axioms). For each system we provide
                   a syntactic proof of cut elimination and a proof of
  URL = {},
  YEAR = 2004

  AUTHOR = {Baratella, S. and Masini, A.},
  TITLE = {An infinitary variant of Metric Temporal Logic over
                   dense time domains},
  JOURNAL = {Mathematical Logic Quarterly},
  VOLUME = {50},
  PAGES = {249--257},
  ABSTRACT = {We introduce a complete and cut-free proof system for
                   a sufficiently expressive fragment of Metric Temporal
                   Logic over dense time domains in which a schema of
                   induction is provable. So doing we extend results
                   previously obtained by Montagna et al. to unbounded
                   temporal operators.},
  URL = {},
  YEAR = 2004

  AUTHOR = {Baratella, S. and Masini, A.},
  TITLE = {A way of making intensional quantification explicit},
  JOURNAL = {Logic Journal of the IGPL},
  ABSTRACT = {We introduce the intensional logic IQL whose main
                   feature is the capability of recovering modal operator
                   Box by means of a genuine first--order quantification
                   over worlds and of an intensional operator (the two
                   components behaving independently). We prove that IQL
                   is sound and complete with respect to an adequate class
                   of structures and that it is decidable. We further show
                   that IQL is a conservative extension of modal system K
                   and of monadic predicate calculus up to
                   interpretability. Eventually we introduce a simple
                   proof system in natural deduction style for IQL},
  URL = {},
  YEAR = 2004

  AUTHOR = {Baratella, S. and Masini, A.},
  TITLE = {A Proof-theoretic Investigation of a Logic of
  JOURNAL = {Annals of Pure and Applied Logic},
  VOLUME = {123},
  PAGES = {135--162},
  ABSTRACT = {We introduce an extension of natural deduction that is
                   suitable for dealing with modal operators and
                   induction. We provide a proof reduction system and we
                   prove a strong normalization theorem for an
                   intuitionistic calculus. As a consequence we obtain a
                   purely syntactic proof of consistency. We also present
                   a classical calculus and we relate provability in the
                   two calculi by means of an adequate formula
  URL = {},
  YEAR = 2003

  AUTHOR = {Franco Barbanera and {de'} Liguoro, Ugo },
  TITLE = {Type Assignement for Mobile Objects},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  ABSTRACT = {We address the problem of formal reasoning about
                   mobile code. We consider an Ambient Calculus, where
                   process syntax includes constructs for sequential
                   programming. For the sake of concreteness, and because
                   of practical relevance, we consider objects using
                   message exchange to implement method invocation and
                   overriding. The contribution of the paper is a type
                   assignment system, obtained by combination of systems
                   for MA and for the Sigma-calculus. We exploit in the
                   mobility framework a typical feature of the
                   intersection type discipline for object calculi, namely
                   late typing of self. The proposed system is then
                   checked against standard properties of related systems,
                   establishing type invariance a completeness theorems.},
  PUBLISHER = {Elsevier},
  URL = {},
  YEAR = 2003

  AUTHOR = {Coppola, Paolo and Ronchi Della Rocca, Simona},
  TITLE = {Principal Typing for Elementary Affine Logic},
  BOOKTITLE = {Typed Lambda Calculi and Applications: 6th
                   International Conference (TLCA 2003)},
  EDITOR = {Hofmann M.},
  VOLUME = {2701},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {90-104},
  ADDRESS = {Berlin},
  PUBLISHER = {Springer-Verlag},
  NOTE = {A preliminary version has been presented at the
                   workshop ``LL---Linear Logic'', affiliated to FLoC'02,
  ABSTRACT = {Elementary Affine Logic (EAL) is a variant of the
                   Linear Logic characterizing the computational power of
                   the elementary bounded Touring machines. The EAL Type
                   Inference problem is the problem of automatically
                   assign to terms of lambda-calculus EAL formulas as
                   types. This problem is proved to be decidable, and an
                   algorithm is showed, building, for every lambda-term,
                   either a negative answer or a finite set of type
                   schemata, from which all and only its typings can be
                   derived, through suitable operations.},
  DISABBLED-ADDRESS = {Valencia, Spain},
  DISABLED-DATA = {10-12,june},
  PDF = {},
  URL = {},
  YEAR = 2003

  AUTHOR = {Dal Lago, Ugo},
  TITLE = {On the Expressive Power of Light Affine Logic},
  BOOKTITLE = {Eight Italian Conference on Theoretical Computer
                   Science, Proceedings},
  EDITOR = {Carlo Blundo and Cosimo Laneve},
  VOLUME = {2841},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {216--227},
  PUBLISHER = {Springer},
  ABSTRACT = {Light Affine Logic (LAL) is a formal system derived
                   from Linear Logic that is claimed to correspond,
                   through the Curry-Howard Isomorphism, to the class
                   FPTIME of polytime functions. The completeness of the
                   system with respect to FPTIME has been proved by
                   embedding different presentations of this complexity
                   class into LAL. The dual property of polytime
                   soundness, on the other hand, has been stated and
                   proved in a more debatable way, depending crucially on
                   the underlying coding scheme. In this paper, we
                   introduce two relevant classes of coding schemes,
                   namely uniform and canonical coding schemes. We then
                   investigate on the equality between FPTIME and the
                   classes of functions that are representable LAL using
                   these coding schemes, obtaining a positive and a
                   negative result.},
  URL = {},
  YEAR = 2003

  AUTHOR = {Dal Lago, Ugo and Martini, Simone},
  TITLE = {Phase Semantics and Decidability of Elementary Affine
  JOURNAL = {Theoretical Computer Science},
  NOTE = {To appear},
  ABSTRACT = {Light, elementary and soft linear logics are formal
                   systems derived from Linear Logic, enjoying remarkable
                   normalization properties. In this paper we prove
                   decidability of Elementary A ne Logic, EAL. The result
                   is obtained by semantical means, first defining a class
                   of phase models for EAL and then proving soundness and
                   (strong) completeness, following Okada s technique.
                   Phase models for Light A ne Logic and Soft Linear Logic
                   are also defined and shown complete.},
  URL = {},
  YEAR = 2004

  AUTHOR = {Dal Lago, Ugo and Martini, Simone and Roversi, Luca},
  TITLE = {Higher Order Linear Ramified Recurrence},
  BOOKTITLE = {Types Conference, Post-Workshop Proceedings},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  NOTE = {To appear},
  ABSTRACT = {Higher-Order Linear Ramified Recurrence (HOLRR) is a
                   linear (affine) lambda-calculus --- every variable
                   occurs at most once --- extended with a recursive
                   scheme on free algebras. One simple condition on type
                   derivations enforces both polytime completeness and a
                   strong notion of polytime soundness on typable terms.
                   Completeness for poly-time holds by embedding Leivant's
                   ramified recurrence on words into HOLRR. Soundness is
                   established at all types --- and not only for first
                   order terms. Type connectives are limited to tensor and
                   linear implication. Moreover, typing rules are given as
                   a simple deductive system},
  URL = {},
  YEAR = 2004

  AUTHOR = {Dezani-Ciancaglini, Mariangiola and Ghilezan, Silvia
                   and Likavec, Silvia},
  TITLE = {Behavioural inverse limit lambda-models},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  NUMBER = {},
  PAGES = {},
  NOTE = {To appear},
  ABSTRACT = {We construct two inverse limit lambda-models which
                   completely characterise sets of terms with similar
                   computational behaviours: the sets of normalising, head
                   normalising, weak head normalising lambda-terms, those
                   corresponding to the persistent versions of these
                   notions, and the sets of closable, closable
                   normalising, and closable head normalising
                   lambda-terms. More precisely, for each of these sets of
                   terms there is a corresponding element in at least one
                   of the two models such that a term belongs to the set
                   if and only if its interpretation (in a suitable
                   environment) is greater than or equal to that element.
                   We use the finitary logical description of the models,
                   obtained by defining suitable intersection type
                   assignment systems, to prove this.},
  KEYWORDS = {Lambda calculus, intersection types, models of lambda
                   calculus, Stone dualities, reducibility method},
  URL = {},
  YEAR = 2004

  AUTHOR = {Dezani-Ciancaglini, Mariangiola and Honsell, Furio and
                   Alessi, Fabio},
  TITLE = {A complete characterization of complete
                   intersection-type preorders},
  JOURNAL = {ACM Transactions on Computational Logic},
  VOLUME = {4(1)},
  PAGES = {120-147},
  ABSTRACT = {We characterize those type preorders which yield
                   complete intersection type assignment systems for
                   lambda calculi, with respect to the thrree
                   set-theoretical semantics for intersection types: the
                   inference semantics, the simple semantics and the
                   F-semantics. These semantics arise by taking as
                   interpretation of types subsets of applicative
                   structures, as interpretation of the preorder relation
                   set theoretic inclusion, as interpretation of
                   intersection constructor set theoretic intersection,
                   and by taking as interpretation of the arrow
                   constructor, the arrow  la Scott, with respect to
                   either any possible functionality set, or the largest
                   one, or the least one. These result strengthen and
                   generalize significantly all earlier results in the
                   literature, to ou knowledge, in at least three
                   respects. First of all the inference semantics had not
                   been considered before. Secondly, the characterizations
                   are all given just in terms of simple closure
                   conditions on the preorder relation on the types,
                   rather than on the typing judgments themselves. The
                   task of checking the condition is made therefore
                   considerably more tractable. Lastly, we do not restrict
                   attention just to lambda models, but to arbitrary
                   applicative structures which admit an interpretation
                   function. Thus we allow also for the treatment of
                   models or restricted lambda calculi. Nevertheless the
                   characterization we give can be tailored just to the
                   case of lambda models. },
  URL = {},
  YEAR = 2003

  AUTHOR = {F.Honsell and M. Lenisa},
  TITLE = {Wave-style Geometry of Interaction Models in Rel are
                   Graph-like Lambda Models},
  BOOKTITLE = {Proceedings of TYPES'03},
  VOLUME = {},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {},
  PUBLISHER = {Springer Verlag},
  ABSTRACT = {We study the connections between graph models and
                   ``wave-style'' Geometry of Interaction (GoI)
                   lambda-models. The latters arise when Abramsky's GoI
                   axiomatization, which generalizes Girard's original
                   GoI, is applied to a traced monoidal category with the
                   categorical product as tensor, using a countable power
                   as the traced strong monoidal functor bang. Abramsky
                   hinted that the category Rel of sets and relations is
                   the basic setting for traditional denotational ``static
                   semantics''. However, the category Rel together with
                   the cartesian product apparently escapes original
                   Abramsky's axiomatization. Here we show that, by moving
                   to the category Rel* of pointed sets and relations
                   preserving the distinguished point, and by sligthly
                   relaxing Abramsky's GoI axiomatization, we can recover
                   a large class of graph-like models as wave models.
                   Furthermore, we show that the class of untyped
                   lambda-theories induced by wave-style GoI models is
                   richer than that induced by game models.},
  URL = {},
  YEAR = 2003

  AUTHOR = {F.Honsell and M. Lenisa and R. Redamalla},
  TITLE = {Strict Geometry of Interaction Graph Models},
  BOOKTITLE = {Proceedings of LPAR'03},
  VOLUME = {2850},
  SERIES = {Lecture Notes in Artificial Intelligence},
  PAGES = {403--417},
  PUBLISHER = {Springer Verlag},
  ABSTRACT = {We study a class of ``wave-style'' Geometry of
                   Interaction (GoI) lambda-models based on the category
                   Rel of sets and relations. Wave GoI models arise when
                   Abramsky's GoI axiomatization, which generalizes
                   Girard's original GoI, is applied to a traced monoidal
                   category with the categorical product as tensor, using
                   ``countable power'' as the traced strong monoidal
                   functor bang. Abramsky hinted that the category Rel is
                   the basic setting for traditional denotational ``static
                   semantics''. However, Rel, together with the cartesian
                   product, apparently escapes Abramsky's original GoI
                   construction. Here we show that Rel can be axiomatized
                   as a strict GoI situation, i.e. a strict variant of
                   Abramsky's GoI situation, which gives rise to a rich
                   class of strict graph models. These are models of
                   restricted lambda-calculi in the sense of [HL99], such
                   as Church's lambda-I-calculus and the
  URL = {},
  YEAR = 2003

  AUTHOR = {Guerrini, Stefano and Martini, Simone and Masini,
  TITLE = {Coherence for sharing proof-nets},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = {294},
  PAGES = {379--409},
  YEAR = 2003

  AUTHOR = {Loreti, P. and Pedicini, M.},
  TITLE = {An object oriented approach to idempotent analysis:
                   Integral Equations as Optimal Control Problems},
  BOOKTITLE = {Proceedings of the International Workshop on
                   Idempotent Mathematics nnd Mathematical Physics,
                   International Erwin Schroedinger Institute (2003), AMS},
  SERIES = {Contemporary Mathematics},
  ABSTRACT = { Within the framework of generic programming, we
                   implement an abstract algorithm for solution of an
                   integral equation of second kind with the resolvent
                   kernels method. Then, as an application of the
                   idempotent analysis analog of resolvent kernels
                   developed in cite{LoretiPedicini2001}, we apply the
                   algorithm to the numerical solution of an optimal
                   control problem with stopping time. },
  NOTES = {to appear},
  URL = {},
  YEAR = 2004

  AUTHOR = {Loreti, P. and Pedicini, M.},
  TITLE = {Idempotent analogue of resolvent kernels for a
                   deterministic optimal control problem},
  JOURNAL = {Mat. Zametki},
  VOLUME = {69},
  NUMBER = {2},
  PAGES = {235--244},
  ABSTRACT = { A solution of a discrete Hamilton Jacobi Bellman
                   equation is represented in terms of idempotent analysis
                   as a convergent series of integral operators. },
  FJOURNAL = {Rossi\u\i skaya Akademiya Nauk. Matematicheskie
  ISSN = {0025-567X},
  MRCLASS = {49L20 (49K15)},
  MRNUMBER = {2002d:49038},
  MRREVIEWER = {A. M. Tarasyev},
  URL = {},
  YEAR = 2001

  AUTHOR = {Maieli, Roberto and Puite, Quintijn},
  TITLE = {Modularity of Proof-nets: generating the type of a
  JOURNAL = {Archive for Mathematical Logic},
  VOLUME = {to appear},
  NUMBER = {},
  PAGES = {},
  ABSTRACT = {When we cut a multiplicative proof-net of linear logic
                   in two parts we get two modules with a certain border.
                   We call pretype of a module the set of partitions over
                   its border induced by Danos-Regnier switchings. The
                   type of a module is then defined as the double
                   orthogonal of its pretype. This is an optimal notion
                   describing the behaviour of a module: two modules
                   behave in the same way precisely if they have the same
                   type. In this paper we define a procedure which allows
                   to characterize (and calculate) the type of a module
                   only exploiting its intrinsic geometrical properties
                   and without any explicit mention to the notion of
                   orthogonality. This procedure is simply based on
                   elementary graph rewriting steps, corresponding to the
                   associativity, commutativity and weak-distributivity of
                   the multiplicative connectives of linear logic.},
  URL = {},
  YEAR = 2004

  AUTHOR = {Mazza, Damiano},
  TITLE = {Logica lineare e complessit\`a computazionale},
  SCHOOL = {Universit\`a degli Studi Roma Tre, Rome},
  TYPE = {Tesi di laurea},
  URL = {},
  YEAR = 2002

  AUTHOR = {Mazza, Damiano},
  TITLE = {Notes on light linear logic},
  INSTITUTION = {Institut de Math\'ematiques de Luminy},
  URL = {},
  YEAR = 2003

  AUTHOR = {Paolini, Luca},
  TITLE = {Lambda-theories: some investigations},
  SCHOOL = {Universit\`a di Genova and Universit\'e de la
  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, 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. It is proved that it enjoys the confluence
                   property, and a necessary and sufficient condition is
                   given, under which it enjoys the standardization
                   property. Hence, we extended some basic syntactical
                   notion of the classical lambda-calculus to the
                   parametric lambdaDelta-calculus such as solvability,
                   separability, theory. We have studied the notions of
                   solvability and separability in the call-by-value
                   setting; unfortunately, there is no evidence on how
                   treat this kind of notions in an unified way for our
                   parametric lambdaDelta-calculus. On the other hand, we
                   are able to show that some property on theories hold
                   for each lambdaDelta-calculus. The notion of
                   solvability in the call-by-value lambda-calculus has
                   been defined and completely characterized, after the
                   preliminary characterization of the class of
                   potentially valuable terms. It turns out that the
                   call-by-value reduction rule (the beta_v-reduction of
                   Plotkin) is too weak for capturing the solvability
                   property of terms, so some new reduction has been
                   defined in order to do this. The notion of separability
                   is the key notion used in the B\"ohm Theorem, proving
                   that syntactically different beta-eta-normal forms are
                   separable in the classical lambda-calculus endowed with
                   beta-reduction, i.e. in the call-by-name setting. In
                   the case of call-by-value lambda-calculus endowed with
                   beta_v-reduction and eta_v-reduction, it turns out that
                   two syntactically different beta-eta-normal forms are
                   separable too, while the notions of beta_v-normal form
                   and eta_v-normal form are semantically meaningless.\\
                   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. It is showed that they can
                   be instantiated in order to give the more interesting
                   operational reduction machines of untyped
                   lambda-calculi. This kind of operational semantics
                   induces theories correct for the related
                   lambda-Delta-calculus. We study some property of the
                   main instances of Delta and Theta. We have defined some
                   parametric notion, as that of relevant contexts,
                   operational extensionality and head-discriminability,
                   hence we try to find some general characterization. It
                   is showed that the standard operational equivalence
                   induced from the Plotkin's call-by-value
                   lambda-calculus is not semisensible, namely there there
                   is a solvable term equated to an unsolvable one. 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. This kind of model is built by
                   introducing the key notion of orthogonality, similar to
                   that used in the Girard's phase semantics and ludics.
                   By mimicking in an awful manner the Girard work, our
                   notion of orthogonality opposes lambda-terms to
                   contexts. Furthermore, we have showed a partial
                   characterization of the orthogonality induced from the
                   evaluation of terms to head normal form, in the
                   classical call-by-name lambda-calculus.\\ In the last
                   part, we have studied a typed lambda-calculus with
                   constants (PCF-like) and its standard interpretation on
                   coherent spaces and stable functions. It is well-know
                   that the model is not fully abstract with respect to
                   the standard operational semantics, since the
                   Scott-continuous Gustave function. We have showed that
                   in coherent spaces there is some stable function that
                   is not Scott-continuous already in finite domains, thus
                   these functions are independent from that of Gustave
                   that is continuous. Hence, we have extended both the
                   syntax and the operational semantics of the considered
                   language and we have showed that the interpretation of
                   the extended language becomes fully abstract with
                   respect to the standard interpretation on coherent
                   spaces. Thus an operational characterization of stable
                   functions (having domain/codomain on coherent spaces
                   being interpretation on types of the language) is
                   given. After we have developped the results of this
                   part of the thesis, we have discovered that the same
                   problem was considered first by Jim and Meyer, on
                   dI-domains. They have showed some negative results.
                   First they define in a denotational way some stable
                   non-Scott-continuous function similar to our one, hence
                   they show that this operator break-down the coincidence
                   between the applicative-preorder on terms and the
                   contextual-preorder. Finally, they show that with their
                   huge class of ``linear ground operational rules''
                   defining some PCF-like rules of evaluation, the before
                   considered coincidence, cannot be break-down. So they
                   conclude that it is hard to find an extension of PCF
                   endowed with operators having a meaningful operational
                   description being fully abstract with respect to stable
                   functions. Although, one of the operators that we add
                   to PCF fall down from their PCF-like rules, we think
                   that its meaning is rather clear.\\ },
  URL = {},
  YEAR = 2003

  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},
  ABSTRACT = {A lambda-calculus is defined, which is parametric with
                   respect to a set V 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 V and a set W of output values. },
  URL = {},
  YEAR = 2004

  AUTHOR = {Paolini, Luca and Ronchi Della Rocca, Simona},
  TITLE = {Lazy logical semantics},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  ABSTRACT = {The lazy evaluation of the lambda-calculus, both in
                   call-by-name and in call-by-value setting, is studied.
                   Starting from a logical descriptions of two topological
                   models of such calculi, a pre-order relation on terms,
                   stratified by types, is defined, which grasps exactly
                   the two operational semantics we want to model. Such a
                   relation can be used for building two fully abstract
  PUBLISHER = {Elsevier},
  URL = {},
  YEAR = 2003

  AUTHOR = {Pedicini, M. and Quaglia, F.},
  TITLE = {{PELCR}: {Parallel Environment for optimal Lambda
                   Calculus Reduction}},
  NOTE = {in preparation}

  AUTHOR = {Pedicini, M. and Quaglia, F.},
  TITLE = {Scheduling vs. Communication in {PELCR}},
  BOOKTITLE = {Euro-Par'2002 - Parallel Processing, (Paderborn 2002)},
  PUBLISHER = {Springer},
  VOLUME = {2400},
  SERIES = {Lecture Notes in Comput. Sci.},
  PAGES = {648-654},
  ADDRESS = {Berlin},
  ABSTRACT = { PELCR is an environment allowing reduction of
                   $\lambda$-terms on parallel/distributed computing
                   systems. The computation performed in this environment
                   is a distributed graph rewriting and a major
                   optimization to achieve efficient execution consists of
                   a message aggregation technique exhibiting the
                   potential for strong reduction of the communication
                   overhead. In this paper we discuss the interaction
                   between the effectiveness of aggregation and the
                   schedule sequence of rewriting operations. Then we
                   present a Priority Based (BP) scheduling algorithm well
                   suited for the specific aggregation technique.
                   Experimental results on a classical benchmark
                   $\lambda$-term demonstrate the benefits from PB in
                   allowing PELCR to achieve up to 88\% of the ideal
                   speedup while executing on a shared memory parallel
                   architecture. },
  URL = {},
  YEAR = 2002

  AUTHOR = {Pedicini, M. and Quaglia, F.},
  TITLE = {A parallel implementation for optimal lambda-calculus
  BOOKTITLE = {2nd International Conference on Principles and
                   Practice of Declarative Programming (PPDP 2000,
  PUBLISHER = {ACM Press},
  SERIES = {ACM Proceedings},
  PAGES = {3-14},
  ADDRESS = {Berlin},
  ABSTRACT = {In this paper we present a parallel implementation of
                   L\'evy's \emph{optimal reduction} for the
                   $\lambda$-calculus cite{Lev78}. In a similar approach
                   to Lamping's one in \cite{Lamping90}, we base our work
                   on a graph reduction technique known as \emph{directed
                   virtual reduction} cite{DPR97} which is actually a
                   restriction of Danos-Regnier virtual reduction
                   cite{DanosRegnier93}. The parallel implementation
                   relies on a strategy for directed virtual reduction,
                   namely {\em half combustion}, which we introduce in
                   this paper. We embed in the implementation both a
                   message aggregation technique, allowing a reduction of
                   the communication overhead, and a fair policy for
                   distributing dynamically originated load among
                   processors. The aggregation technique is mandatory as
                   the granularity of the computation is fine. Through
                   this technique we obtain a linear speedup close to 80\%
                   of the ideal one on a shared memory multiprocessor.
                   This result points out the viability of parallel
                   implementations for optimal reduction. },
  URL = {},
  YEAR = 2000

  AUTHOR = {Pedicini, Marco},
  TITLE = {Greedy Expansions and Sets with Deleted Digits},
  ABSTRACT = {We generalize a result of Dar{\'o}czy and K{\'a}tai,
                   on the characterization of univoque numbers with
                   respect to a non-integer base [Dar{\'o}czyK{\'a}ta1985]
                   by relaxing the digits alphabet to a generic set of
                   real numbers. We apply the result to derive the
                   construction of a B\"uchi automata accepting all and
                   only the greedy sequences for a given base and digit
                   set. In the appendix we prove a more general version of
                   the fact that the expansion of an element $x\in QQ(q)$
                   is possibly periodic, if $q$ is a Pisot number. },
  URL = {}

  AUTHOR = {Pedicini, Marco and Puite, Quintijn},
  TITLE = {On the number of provable formulas},
  NOTE = {in preparation},
  ABSTRACT = {This work is a first step in the study of
                   combinatorics of proof nets: proof nets are pure
                   geometrical objects issued from the study of linear
                   logic, they are intended to capture the non-burocratic
                   aspects of proofs in sequent calculus; in fact, they
                   can be obtained from proof structures (pure
                   combinatorial nets of rules (or links)) by adding a
                   constraint known as ``correctness criterion'' (usually
                   cited in the Danos-Regnier form). We try to establish
                   the exact ratio between proof structures and proof
                   nets, finally we can obtain only an upperbound and a
  YEAR = 2002

  AUTHOR = {Elaine Pimentel and Simona Ronchi della Rocca and Luca
  TITLE = {Towards a proof-theoretical justification for
                   Intersection Types},
  INSTITUTION = {Dipartimento di Informatica, Universit\`a di Torino},
  TYPE = {Technical Report},
  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.},
  URL = {},
  YEAR = 2004

  AUTHOR = {Ronchi Della Rocca, Simona},
  TITLE = {Typed {I}ntersection {L}ambda {C}alculus},
  BOOKTITLE = {L{TRS} 2002},
  VOLUME = {70(1)},
  SERIES = {Electronic Notes in Computer Science},
  PAGES = {},
  PUBLISHER = {Elsevier},
  ABSTRACT = {The aim of this paper is to discuss the design of an
                   explicitly typed lambda-calculus corresponding to the
                   Intersection Type Assignment System (IT), which assigns
                   intersection types to the untyped lambda-calculus. Two
                   different proposals are given. The logical foundation
                   of all of them is the Intersection Logic
  PDF = {},
  URL = {},
  YEAR = 2002

  AUTHOR = {Ronchi Della Rocca, Simona and Paolini, Luca},
  TITLE = {The parametric lambda-calculus: a metamodel for
  PUBLISHER = {Springer-Verlag},
  SERIES = {Computer Science -- Monograph},
  NOTE = {Ed. Ingeborg Mayer},
  ABSTRACT = {The book is divided in four parts.\\ The first part is
                   devoted to the study of the syntax of
                   lambda-Delta-calculus. Some syntactical properties,
                   like confluence and standardization, can be studied for
                   the whole Delta class. Other properties, like
                   solvability and separability, cannot be treated in an
                   uniform way, and they are therefore introduced
                   separately for different instances of Delta. \\ In the
                   second part the operational semantics of
                   lambda-Delta-calculus is studied. The notion of
                   operational semantics can be given in a parametric way,
                   by supplying not only a set of input values but also a
                   set of output values Theta, enjoying some very natural
                   properties. A universal reduction machine is defined,
                   parametric into both Delta and Theta, enjoying a sort
                   of correctness property in the sense that, if a term
                   can be reduced to an output value, then the machine
                   stops, returning a term operationally equivalent to it.
                   Then four particular reduction machines are presented,
                   three for the call-by-name lambda-calculus and one for
                   the call-by-value lambda-calculus, thereby four
                   operational behaviours that are particularly
                   interesting for modelling programming languages.
                   Moreover, the notion of extensionality is revised,
                   giving a new parametric definition that depends on the
                   operational semantics we want to consider. \\ The third
                   part is devoted to denotational semantics. The general
                   notion of model of lambda\Delta-calculus is defined,
                   and then the more restrictive and useful notion of
                   filter model, based on intersection types, is given.
                   Then four particular filter models are presented, each
                   one correct with respect to one of the operational
                   semantics studied in the previous part. For two of them
                   completeness is also proved. The other two models are
                   incomplete: we prove that there are no filter models
                   enjoying the completeness property with respect to
                   given operational semantics, and we build two complete
                   models by using a technique based on intersection
                   types. Moreover, the relation between filter models and
                   Scott's model is given. \\ The fourth part deals with
                   the computational power of lambda-Delta-calculus. It is
                   well known that lambda-calculus is Turing complete, in
                   both its call-by-name and call-by-value variants, i.e.
                   it has the power of the computable functions. Here we
                   prove something more, namely that each one of the
                   reduction machines we present in the third part of this
                   book can be used for computing all the computable
                   functions. },
  URL = {},
  YEAR = 2004

  AUTHOR = {Ronchi Della Rocca, Simona and Roversi, Luca},
  TITLE = {Intersection {L}ogic},
  BOOKTITLE = {Proceedings of {CSL'01}},
  VOLUME = {2412},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {414 -- 428},
  ADDRESS = {},
  PUBLISHER = {Springer Verlag},
  ABSTRACT = { The intersection type assignment system IT uses the
                   formulas of the negative fragment of the predicate
                   calculus (LJ) as types for the terms. However, the
                   deductions of IT only correspond to the proper subset
                   of the derivations of LJ obtained by imposing a
                   meta-theoretic condition about the use of the
                   conjunction of LJ. This paper proposes a logical
                   foundation for IT. This is done by introducing a logic
                   IL. Intuitively, a derivation of IL is a set of
                   derivations in LJ such that the derivations in the set
                   can be thought of as writable in parallel. This way of
                   looking at LJ, by means of IL, means that the
                   meta-theoretic condition mentioned above can be
                   transformed into a purely structural property of IL.
                   The relation between IL and LJ surely has a first main
                   benefit: the strong normalization of LJ directly
                   implies the same property on IL, which translates into
                   a very simple proof of the strong normalizability of
                   the terms typable with IT. },
  MONTH = {},
  URL = {},
  YEAR = 2001

  AUTHOR = {Ugo Solitro},
  TITLE = {An interaction calculus for concurrent systems},
  INSTITUTION = {Dipartimento di Informatica - Universita' degli Studi
                   di Verona},
  NUMBER = {RR 15/2004},
  ADDRESS = {Strada Le Grazie, 15 -- I-37134 Verona (Italy)},
  ABSTRACT = {In this work we describe a simple calculus (called
                   interaction calculus) for the representation of
                   concurrent systems. In this a system is collection of
                   expressions (processes) that share a working space;
                   their computational behaviour is determined by the
                   interaction of processes. The calculus is an attempt to
                   describe concurrent systems by means of a ``non
                   functional'' calculus which is, in some sense, strictly
                   related with the lambda-calculus: computations are
                   carried out by substitutions, but in our calculus they
                   are originated by a symmetric interaction between two
                   expressions, instead of the functional application of
                   an operator to its operand. In this way we lose some
                   good features of lambda calculus (the confluence
                   property for instance), but we gain the capability of
                   representing concurrency and mobility; all the same, we
                   will discover that functions can be nicely encoded in
                   the calculus.},
  KEYWORDS = {Concurrency, lambda calculus, interaction, linear
  URL = {},
  YEAR = 2004

  AUTHOR = {Myriam Quatrini and Tortora de Falco, Lorenzo},
  TITLE = {Polarisation des preuves classiques et renversement},
  JOURNAL = {Compte-Rendu de l'Acad\'emie des Sciences de {P}aris},
  YEAR = {1996},
  VOLUME = {323},
  PAGES = {113--116},
  URL = {},
  ABSTRACT = {We introduce a new constraint on the proofs of the
classical sequent calculus $LK^\eta_{pol}$ ($\eta$-constrained and
polarized). We obtain a complete and stable fragment for which the $P$
embedding into linear logic is a decoration.}

  AUTHOR = {Tortora de Falco,Lorenzo},
  TITLE = {Denotational semantics for polarized (but
non-constrained) {$LK$} by means of the additives},
  BOOKTITLE = {$5^{th}$ Kurt Goedel Colloquium KGC'97, computational
logic and                proof theory},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1289},
  PAGES = {290--304},
  YEAR = {1997},
  URL = {},
  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 non-constrained
$LK$ in linear logic, which induces a denotational semantics. A
classical cut-elimination step is now a cut-elimination step in one of
the `constructive slices' superimposed by the classical proof.}

  AUTHOR = {Tortora de Falco,Lorenzo},
  TITLE = {Additives of linear logic and normalization- Part {I}: a 
             (restricted) Church-Rosser property},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = {294/3},
  PAGES = {489--524},
  YEAR = {2003},
  URL = {},
  ABSTRACT = {We define a generalized cut-elimination procedure for
proof-nets of full linear logic (without constants), for which we prove
a (restricted) Church-Rosser property.}

  AUTHOR = {Jean-Baptiste Joinet and Harold Schellinx and Tortora
de Falco, Lorenzo},
  TITLE = {{SN} and {CR} for free-style ${LK}^{tq}$: linear
decorations and simulation of normalization},
  JOURNAL = {Journal of Symbolic Logic},
  VOLUME = {67 (1)},
  PAGES = {162--196},
  YEAR = {2002},
  URL = {},
  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
type-distinction}\/ 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.}

  AUTHOR = {Olivier Laurent and Myriam Quatrini and Tortora de Falco,
  TITLE = {Polarized and Focalized Linear and Classical proofs},
  JOURNAL = {Annals of Pure and Applied Logic},
  YEAR = {2000},
  NOTE = {to appear},
  URL = {},
  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 tq-protocol of normalization 
 for the classical systems $LKe$ and $LKer$ perfectly fits
normalization of polarized proof-nets. In section ref{isos}, some more
semantical considerations allow to recover $LC$ as a reinement of
multiplicative LKe}

  AUTHOR = {Tortora de Falco, Lorenzo},
  TITLE = {The additive multiboxes},
  JOURNAL = {Annals of Pure and Applied Logic},
  VOLUME = {120, Issue 1-3},
  PAGES = {65--102},
  YEAR = {2003},
  URL = {},
  ABSTRACT = {We introduce the new notion of additive ``multibox'' for
linear logic proof-nets. Thanks to this notion, we define a
cut-elimination procedure which associates with every proof-net of
multiplicative and additive linear logic a unique cut-free one.}

  AUTHOR = {Tortora de Falco, Lorenzo},
  TITLE = {Obsessional experiments for Linear Logic Proof-nets},
  JOURNAL = {Mathematical Structures in Computer Science},
  VOLUME = {13, Issue 1},
  PAGES = {799--855},
  YEAR = {2003},
  URL = {},
  ABSTRACT = {We address the question of injectivity of coherent
semantics of linear logic proof-nets. Starting from the definition of
experiment given by Girard, we introduce the key-notion of ``injective
obsessional experiment'', which allows to give a positive answer to our
question for certain fragments of linear logic, and to build
counter-examples to the injectivity of coherent semantics in the general

  AUTHOR = {Olivier Laurent and Tortora de Falco, Lorenzo},
  TITLE = {Slicing polarized additive normalization},
  INSTITUTION = {Istituto per le Applicazioni del Calcolo},
  YEAR = {2001},
  TYPE = {Quaderno},
  NUMBER = {12},
  ADDRESS = {Roma, Italy},
  NOTE = {To appear in \textit{"Linear Logic in Computer
Science", Thomas Ehrhard, Jean-Yves Girard, Paul Ruet and Phil Scott
editors}, London Mathematical Society Lecture Notes Series, Cambridge
University Press},
  URL = {},
  ABSTRACT = {To attack the problem of ``computing with the additives'',
we introduce a notion of sliced proof-net 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 proof-nets, and prove injectivity for the
fragment of polarized linear logic corresponding to simply typed
lambda-calculus with pairing.}

This file has been generated by bibtex2html 1.60       >>> BackToHomePage(Protocollo) <<<