@COMMENT{{ThisfilehasbeengeneratedbyPybliographer}} @INPROCEEDINGS{ABD03, AUTHOR = {Alessi, Fabio and Barbanera, Franco and Dezani-Ciancaglini, Mariangiola}, TITLE = {Intersection Types and Computational Rules}, BOOKTITLE = {WoLLIC'03}, EDITOR = {de Queiroz, Ruy and Pimentel, Elaine and Figueiredo, Lucilia}, NUMBER = {84}, SERIES = {El. Notes in Theoret. Comput. Sci.}, PAGES = {}, ADDRESS = {}, ORGANIZATION = {}, 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 = {http://www.di.unito.it/~dezani/}, YEAR = 2003 } @ARTICLE{AMR03, AUTHOR = {Andreoli, J.M. and Maieli, R. and Ruet, P.}, TITLE = {Constraint-based proof construction in non commutative logic}, JOURNAL = {Theoretical Computer Science}, NOTE = {To appear}, YEAR = 2004 } @UNPUBLISHED{BaillotPedicini2004, AUTHOR = {Baillot, P. and Pedicini, M.}, TITLE = {An embedding of {Blum-Shub-Smale} model of computation in {LLL}}, NOTE = {in preparation} } @ARTICLE{BaillotPedicini2001, 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.}, CODEN = {FUINE}, FJOURNAL = {Fundamenta Informaticae}, ISSN = {0169-2968}, MRCLASS = {03F52 (68N18 68Q55)}, MRNUMBER = {2002j:03070}, MRREVIEWER = {Gianfranco Mascari}, URL = {http://www.iac.rm.cnr.it/~marco/papers/2001fuin.ps}, YEAR = 2001 } @UNPUBLISHED{BallarioPedicini2004, AUTHOR = {Ballario, P. and Pedicini, M.}, TITLE = {Quantitative operational semantics in formal molecular biology}, NOTE = {in preparation} } @ARTICLE{BMaml, 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 completeness.}, URL = {http://www.di.univr.it/dol/main?ent=persona&id=126}, YEAR = 2004 } @ARTICLE{BMmlq, 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 = {http://www.di.univr.it/dol/main?ent=persona&id=126}, YEAR = 2004 } @ARTICLE{BMljIGPL, 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 = {http://www.di.univr.it/dol/main?ent=persona&id=126}, YEAR = 2004 } @ARTICLE{BMapal, AUTHOR = {Baratella, S. and Masini, A.}, TITLE = {A Proof-theoretic Investigation of a Logic of Positions}, 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 translation.}, URL = {http://www.di.univr.it/dol/main?ent=persona&id=126}, YEAR = 2003 } @ARTICLE{BarbaneradeLiguoro:COMETA-03, 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.}, BOOKTITLE = {{COMETA'03}}, PUBLISHER = {Elsevier}, URL = {http://www.di.unito.it/~deligu/papers/COMETA03.html}, YEAR = 2003 } @INPROCEEDINGS{Coppola+Ronchi:TLCA-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, Copenhagen}, 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 = {http://www.di.unito.it/~ronchi/papers/EA-typing.pdf}, URL = {http://www.di.unito.it/~ronchi/}, YEAR = 2003 } @INPROCEEDINGS{ICTCS2003DLU, 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 = {http://www.cs.unibo.it/people/phd-students/dallago/}, YEAR = 2003 } @ARTICLE{TCS2004, AUTHOR = {Dal Lago, Ugo and Martini, Simone}, TITLE = {Phase Semantics and Decidability of Elementary Affine Logic}, 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 = {http://www.cs.unibo.it/~martini/}, YEAR = 2004 } @INPROCEEDINGS{TYPES2003, 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 = {http://www.cs.unibo.it/~martini/}, YEAR = 2004 } @ARTICLE{dezani-ghi-lika-04, 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 = {http://www.di.unito.it/~likavec/}, YEAR = 2004 } @ARTICLE{adh03, 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 = {http://www.di.unito.it/~dezani/papers/tocl1.ps}, YEAR = 2003 } @INPROCEEDINGS{honsell-lenisa03, 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 = {http://www.dimi.uniud.it/~lenisa/}, YEAR = 2003 } @INPROCEEDINGS{honsell-lenisa-redamalla-03, 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 lambda-beta-KN-calculus.}, URL = {http://www.dimi.uniud.it/~lenisa/}, YEAR = 2003 } @ARTICLE{GMM03, AUTHOR = {Guerrini, Stefano and Martini, Simone and Masini, Andrea}, TITLE = {Coherence for sharing proof-nets}, JOURNAL = {Theoretical Computer Science}, VOLUME = {294}, PAGES = {379--409}, YEAR = 2003 } @INCOLLECTION{LoretiPedicini2004, 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}, PUBLISHER = {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 = {http://www.iac.rm.cnr.it/~marco/papers/2003cm.pdf}, YEAR = 2004 } @ARTICLE{LoretiPedicini2001, 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 Zametki}, ISSN = {0025-567X}, MRCLASS = {49L20 (49K15)}, MRNUMBER = {2002d:49038}, MRREVIEWER = {A. M. Tarasyev}, URL = {http://www.iac.rm.cnr.it/~marco/papers/2001mathnotes.pdf}, YEAR = 2001 } @ARTICLE{MP04, AUTHOR = {Maieli, Roberto and Puite, Quintijn}, TITLE = {Modularity of Proof-nets: generating the type of a module}, 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 = {http://www.dsi.uniroma1.it/~maieli}, YEAR = 2004 } @PHDTHESIS{Mazza:TesiLaurea, AUTHOR = {Mazza, Damiano}, TITLE = {Logica lineare e complessit\`a computazionale}, SCHOOL = {Universit\`a degli Studi Roma Tre, Rome}, TYPE = {Tesi di laurea}, URL = {http://iml.univ-mrs.fr/~mazza/}, YEAR = 2002 } @TECHREPORT{Mazza:LLL, AUTHOR = {Mazza, Damiano}, TITLE = {Notes on light linear logic}, INSTITUTION = {Institut de Math\'ematiques de Luminy}, URL = {http://iml.univ-mrs.fr/~mazza/}, YEAR = 2003 } @PHDTHESIS{tesi, AUTHOR = {Paolini, Luca}, TITLE = {Lambda-theories: some investigations}, SCHOOL = {Universit\`a di Genova and Universit\'e de la M\'editerran\'ee}, 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 = {http://www.di.unito.it/~paolini/}, YEAR = 2003 } @ARTICLE{PaoRdR04, 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 = {http://www.di.unito.it/~paolini/}, YEAR = 2004 } @ARTICLE{PaoRdR03lls, 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 models.}, PUBLISHER = {Elsevier}, URL = {http://www.di.unito.it/~paolini}, YEAR = 2003 } @UNPUBLISHED{PediciniQuaglia2004, AUTHOR = {Pedicini, M. and Quaglia, F.}, TITLE = {{PELCR}: {Parallel Environment for optimal Lambda Calculus Reduction}}, NOTE = {in preparation} } @INCOLLECTION{PediciniQuaglia2002, 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 = {http://www.iac.rm.cnr.it/~marco/papers/2002europar.pdf}, YEAR = 2002 } @INCOLLECTION{PediciniQuaglia2000, AUTHOR = {Pedicini, M. and Quaglia, F.}, TITLE = {A parallel implementation for optimal lambda-calculus reduction}, BOOKTITLE = {2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000, Montreal)}, 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 = {http://www.iac.rm.cnr.it/~marco/papers/2000ppdp.ps}, YEAR = 2000 } @UNPUBLISHED{Pedicini2004, 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 = {http://www.iac.rm.cnr.it/~marco/papers/2003tcs.ps} } @UNPUBLISHED{PediciniPuite2002, 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 lowerbound.}, YEAR = 2002 } @TECHREPORT{PimentelRonchiRoversi:2004, AUTHOR = {Elaine Pimentel and Simona Ronchi della Rocca and Luca Roversi}, 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 = {http://www.dcc.ufmg.br/~pimentel}, YEAR = 2004 } @INPROCEEDINGS{Ronchi:ITRS-2002, 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 IL.}, PDF = {http://www.di.unito.it/~ronchi/papers/ronchi-itrs02.pdf}, URL = {http://www.di.unito.it/~ronchi}, YEAR = 2002 } @BOOK{PaoRdRlibro03, AUTHOR = {Ronchi Della Rocca, Simona and Paolini, Luca}, TITLE = {The parametric lambda-calculus: a metamodel for computation}, 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 = {http://www.di.unito.it/~ronchi}, YEAR = 2004 } @INPROCEEDINGS{ronchi-roversi-01, 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 = {http://www.di.unito.it/~rover/}, YEAR = 2001 } @TECHREPORT{Sol04, 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 logic}, URL = {http://www.di.univr.it/~solitro}, YEAR = 2004 } @ARTICLE{polrenvers, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} } @INPROCEEDINGS{bot, 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}, PUBLISHER = SPRINGER, YEAR = {1997}, URL = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} } @ARTICLE{additifs1, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} } @ARTICLE{freelktq, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} } @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}, YEAR = {2000}, NOTE = {to appear}, URL = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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} } @ARTICLE{multiboxes, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} } @ARTICLE{injectcoh, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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 case.} } @TECHREPORT{slice, 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}, MONTH = JUN, 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 = {http://www.logique.jussieu.fr/www.tortora/papers.html}, 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.} }