biblio.bib
@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.}
}
This file has been generated by
bibtex2html 1.60
>>> BackToHomePage(Protocollo) <<<