dart-reports.bib
@COMMENT{{This file has been generated by bib2bib 1.43}}
@COMMENT{{Command line: /u1/staff/jbw/church/bibtex2html/bib2bib.byte -oc /u1/staff/jbw/gc/gc/www/publications/auto/keys -ob /u1/staff/jbw/gc/gc/www/publications/auto/dart-reports.bib -c dartreport="yes" /u1/staff/jbw/share/share/bibtex/bibliography.bib /u1/staff/jbw/share/share/bibtex/conferences.bib}}
@COMMENT{{PleasedonotputRCS/CVSIdexpansionhere}}
@COMMENT{{***WhoaTOCLseemsliketheabbreviationforTransactions
on Computational Logic.Maybethisisamistake.Checkallentriesusingthisabbreviationtoseeiftheyarecorrect.}}
@INPROCEEDINGS{Liq+Ron:ITRS-2004,
ITRSPAPER = {yes},
DARTREPORT = {yes},
AUTHOR = {Luigi Liquori and Ronchi Della Rocca, Simona},
TITLE = {Towards an Intersection Typed System \textit{{\'a}
la} {C}hurch},
CROSSREF = {ITRS2004},
PDF = {http://www.di.unito.it/~ronchi/papers/itrs-liquori-ronchi.pdf},
ABSTRACT = {In this paper, a fully typed lambda calculus based
on the well-known intersection type system
discipline is presented, based on a type store
storing informations about the structures of types
and a notion of modality, decorating terms,
remembering some informations about the structure of
the type assignment proof. The present system is the
counterpart \textit{{\'a} la} Church of the type assignment
system as invented by Coppo and Dezani}
}
@INPROCEEDINGS{vB+dL:ICTCS-2003,
ITRSPAPER = {yes},
AUTHOR = {S. {van Bakel} and U. {de' Liguoro}},
TITLE = {Logical Semantics for the First Order Sigma-Calculus},
BOOKTITLE = {ICTCS'03},
YEAR = {2003},
SERIES = {LNCS},
VOLUME = {2841},
PAGES = {202--215},
MONTH = OCT,
PUBLISHER = {Springer-Verlag},
PDF = {http://www.di.unito.it/~deligu/pub/vBdL03.pdf},
ABSTRACT = {We investigate logical semantics of the first
order Sigma-calculus.
An assignment system of predicates to first order typed terms of
the OB_1 calculus is introduced. We define
retraction models for that calculus and an interpretation of
terms, types and predicates into such models. The assignment
system is then proved to be sound and complete w.r.t. retraction models.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bar+dL:COMETA-2003,
ITRSPAPER = {yes},
AUTHOR = {F. Barbanera and U. {de' Liguoro}},
TITLE = {Type Assignment for Mobile Objects},
BOOKTITLE = {{COMETA'03}},
YEAR = {2004},
SERIES = {ENTCS 104C},
PUBLISHER = {Elsevier},
DARTREPORT = {yes},
PDF = {http://www.di.unito.it/~deligu/papers/BdL03.pdf},
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.}
}
@CONFERENCE{vanBakeldeLiguoro:ICTCS-05,
AUTHOR = {Steffen van Bakel, Ugo {de' Liguoro}},
TITLE = {Subtyping Object and Recursive Types Logically},
BOOKTITLE = {{Proceedings of ICTCS'05}},
YEAR = {2005},
PUBLISHER = {Springer-Verlag},
SERIES = {LNCS},
PDF = {http://www.di.unito.it/~deligu/papers/vBdL05draft.pdf},
NOTE = {To appear},
ABSTRACT = {Subtyping in first order object calculi is studied with respect
to the logical semantics obtained by identifying terms that satisfy the same
set of predicates, as formalized through an assignment system. It is shown
that equality in the full first order Sigma-calculus is modelled by this
notion, which on turn is included in a Morris style contextual equivalence.},
DARTREPORT = {yes}
}
@UNPUBLISHED{deLiguoro:REP-2002,
ITRSPAPER = {yes},
AUTHOR = {U. de' Liguoro},
TITLE = {Restricted intersection type assignment
systems and object properties},
MONTH = DEC,
YEAR = 2002,
DARTREPORT = {yes},
ABSTRACT = {
In this note we consider a restricted version of the intersection
types for a lambda-calculus with records as presented in
\cite{deLiguoro:TLCA-2001,deLiguoro:ITRS-2002} w.r.t. principal
typing property and expressivity. We sketch how the classical
approach to principal typing for intersection type assignment
system can be adapted to cope with record types. We then exemplify
typings in our system of self-application and recursive record
interpretations of objects.
},
PDF = {http://www.di.unito.it/~deligu/pub/dLRep02.pdf}
}
@TECHREPORT{Amt+Wel:MPD-2002,
AUTHOR = {Torben Amtoft and J. B. Wells},
TITLE = {Mobile Processes with Dependent Communication Types
and Singleton Types for Names and Capabilities},
MONTH = DEC,
YEAR = 2002,
INSTITUTION = {Kansas State University, Department of Computing and
Information Sciences},
NUMBER = {2002-3},
URL = {http://www.cis.ksu.edu/~schmidt/techreport/2002.list.html},
PDF = {http://www.cis.ksu.edu/~tamtoft/Papers/Amt+Wel:MPwDCT-2002/short.pdf},
XNOTE = {Torben has replaced the file supposed linked to as
KSU CIS TR 2002-3 with a later version which was
submitted to SAS '03. The original KSU CIS TR
2002-03 is no longer available!!! It might be
possible to reconstruct something like it via CVS
time travel, but it would be a pain.
Torben, 02/07/04: the link now again points to
the original report!!},
DARTREPORT = {yes},
CHURCHREPORT = {yes},
ABSTRACT = {There are many calculi for reasoning about
concurrent communicating processes which have
locations and are mobile. Examples include the
original Ambient Calculus and its many variants, the
Seal Calculus, the MR-calculus, the M-calculus,
etc. It is desirable to use such calculi to describe
the behavior of mobile agents. It seems reasonable
that mobile agents should be able to follow
non-predetermined paths and to carry
non-predetermined types of data from location to
location, collecting and delivering this data using
communication primitives. Previous type systems for
ambient calculi make this difficult or impossible to
express, because these systems (if they handle
communication at all) have always globally mapped
each ambient name to a type governing the type of
values that can be communicated locally or with
adjacent locations, and this type can not depend on
where the ambient has traveled. \par We present a
new type system where there are no global
assignments of types to ambient names. Instead, the
type of an ambient process $P$ not only indicates
what can be locally communicated but also gives an
upper bound on the possible ambient nesting shapes
of any process $P'$ to which $P$ can evolve, as well
as the possible capabilities and names that can be
exhibited or communicated at each location. Because
these shapes can depend on which capabilities and
names are actually communicated, the types support
this with explicit dependencies on
communication. This system is thus the first type
system for an ambient calculus which provides type
polymorphism of the kind that is usually present in
polymorphic type systems for the
$\lambda$-calculus.}
}
@TECHREPORT{Mak+Wel:TIP-2004,
AUTHOR = {Henning Makholm and J. B. Wells},
TITLE = {Type Inference for {PolyA}},
YEAR = 2004,
MONTH = JAN,
CHURCHREPORT = {yes},
DARTREPORT = {yes},
DISABLEDPDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0013.pdf},
PDF = {http://www.macs.hw.ac.uk/DART/reports/D2.3/MW04.pdf},
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
Sci.},
NUMBER = {HW-MACS-TR-0013},
ABSTRACT = {We present an automatic type inference algorithm for
PolyA, a type system for Mobile Ambients presented
in earlier work by us together with Torben
Amtoft. We present not only a basic inference
algorithm, but also several optimizations to it
aimed at reducing the size of the inferred
types. The final algorithm has been implemented and
verified to work on small examples. We discuss some
small problems that still exist and methods for
solving them.}
}
@TECHREPORT{Amt+Mak+Wel:PolyA-2004a,
AUTHOR = {Torben Amtoft and Henning Makholm and J. B. Wells},
TITLE = {{PolyA}: True Type Polymorphism for {M}obile
{A}mbients},
YEAR = 2004,
MONTH = FEB,
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
Sci.},
NUMBER = {HW-MACS-TR-0015},
PDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0015.pdf},
CHURCHREPORT = {yes},
DARTREPORT = {yes},
NOTE = {A shorter successor is \cite{Amt+Mak+Wel:TCS-2004}},
ABSTRACT = {Previous type systems for mobility calculi (the
original Mobile Ambients, its variants and
descendants, e.g., Boxed Ambients and Safe Ambients,
and other related systems) offer little support for
generic mobile agents. Previous systems either do
not handle communication at all or globally assign
fixed communication types to ambient names that do
not change as an ambient moves around or interacts
with other ambients. This makes it hard to type
examples such as a ``messenger'' ambient that uses
communication primitives to collect a message of
non-predetermined type and deliver it to a
non-predetermined destination.
\par
In contrast, we present our new type system
$\mathsf{PolyA}$. Instead of assigning communication
types to ambient names, $\mathsf{PolyA}$ assigns a
type to each process $P$ that gives upper bounds on
(1) the possible ambient nesting shapes of any
process $P'$ to which $P$ can evolve, (2) the values
that may be communicated at each location, and (3)
the capabilities that can be used at each
location. Because $\mathsf{PolyA}$ can type generic
mobile agents, we believe $\mathsf{PolyA}$ is the
first type system for a mobility calculus that
provides type polymorphism comparable in power to
polymorphic type systems for the
$\lambda$-calculus. $\mathsf{PolyA}$ is easily
extended to ambient calculus variants. A restriction
of $\mathsf{PolyA}$ has principal typings.}
}
@INPROCEEDINGS{Amt+Mak+Wel:TCS-2004,
CHURCHREPORT = {yes},
DARTREPORT = {yes},
AUTHOR = {Torben Amtoft and Henning Makholm and J. B. Wells},
TITLE = {{PolyA}: True Type Polymorphism for {M}obile
{A}mbients},
CROSSREF = {TCS2004},
PAGES = {591--604},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Amtoft+Makholm+Wells:PolyA:True-Type-Polymorphism-for-Mobile-Ambients:TCS-2004.pdf},
NOTE = {A more detailed predecessor is
\cite{Amt+Mak+Wel:PolyA-2004a}},
ABSTRACT = {Previous type systems for mobility calculi (the
original Mobile Ambients, its variants and
descendants, e.g., Boxed Ambients and Safe Ambients,
and other related systems) offer little support for
generic mobile agents. Previous systems either do
not handle communication at all or globally assign
fixed communication types to ambient names that do
not change as an ambient moves around or interacts
with other ambients. This makes it hard to type
examples such as a ``messenger'' ambient that uses
communication primitives to collect a message of
non-predetermined type and deliver it to a
non-predetermined destination.
\par
In contrast, we present our new type system
$\mathsf{PolyA}$. Instead of assigning communication
types to ambient names, $\mathsf{PolyA}$ assigns a
type to each process $P$ that gives upper bounds on
(1) the possible ambient nesting shapes of any
process $P'$ to which $P$ can evolve, (2) the values
that may be communicated at each location, and (3)
the capabilities that can be used at each
location. Because $\mathsf{PolyA}$ can type generic
mobile agents, we believe $\mathsf{PolyA}$ is the
first type system for a mobility calculus that
provides type polymorphism comparable in power to
polymorphic type systems for the
$\lambda$-calculus. $\mathsf{PolyA}$ is easily
extended to ambient calculus variants. A restriction
of $\mathsf{PolyA}$ has principal typings.}
}
@TECHREPORT{Mak+Wel:PolyStar-2004,
AUTHOR = {Henning Makholm and J. B. Wells},
TITLE = {Instant Polymorphic Type Systems for Mobile Process
Calculi: Just Add Reduction Rules and Close},
YEAR = 2004,
MONTH = NOV,
CHURCHREPORT = {yes},
DARTREPORT = {yes},
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
Sci.},
NUMBER = {HW-MACS-TR-0022},
XNOTE = {Available at http://www.macs.hw.ac.uk:8080/},
PDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0022.pdf},
NOTE = {A shorter successor is~\cite{Mak+Wel:ESOP-2005}},
ABSTRACT = {Many different \emph{mobile process calculi} have
been invented, and for each some number of type
systems has been developed. Soundness and other
properties must be proved separately for each
calculus and type system.
\par
We present the \emph{generic} polymorphic type
system Poly$\star$ which works for a wide
range of mobile process calculi. For any calculus
satisfying some general syntactic conditions,
well-formedness rules for types are derived
automatically from the reduction rules and
Poly$\star$ works otherwise unchanged. The
derived type system is automatically sound and often
more precise than previous type systems for the
calculus, due to Poly$\star$'s
\emph{spatial polymorphism}.
\par
We present an implemented type inference algorithm
for Poly$\star$ which automatically
constructs a typing given a set of reduction rules
and a term to be typed. The generated typings are
\emph{principal} with respect to certain natural
type shape constraints.}
}
@INPROCEEDINGS{Mak+Wel:ESOP-2005,
AUTHOR = {Henning Makholm and J. B. Wells},
TITLE = {Instant Polymorphic Type Systems for Mobile Process
Calculi: Just Add Reduction Rules and Close},
CHURCHREPORT = {yes},
DARTREPORT = {yes},
CROSSREF = {ESOP2005},
PAGES = {389--407},
NOTE = {A more detailed predecessor is
\cite{Mak+Wel:PolyStar-2004}},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Makholm+Wells:Instant-Polymorphic-Type-Systems-for-Mobile-Process-Calculi:ESOP-2005.pdf},
ABSTRACT = {Many different \emph{mobile process calculi} have
been invented, and for each some number of type
systems has been developed. Soundness and other
properties must be proved separately for each
calculus and type system. We present the
\emph{generic} polymorphic type system
Poly$\star$ which works for a wide range of
mobile process calculi, including the $\pi$-calculus
and Mobile Ambients. For any calculus satisfying
some general syntactic conditions, well-formedness
rules for types are derived automatically from the
reduction rules and Poly$\star$ works
otherwise unchanged. The derived type system is
automatically sound (i.e., has subject reduction)
and often more precise than previous type systems
for the calculus, due to Poly$\star$'s
\emph{spatial polymorphism}. We present an
implemented type inference algorithm for
Poly$\star$ which automatically constructs
a typing given a set of reduction rules and a term
to be typed. The generated typings are
\emph{principal} with respect to certain natural
type shape constraints.}
}
@TECHREPORT{Mak+Wel:2005-HW-MACS-TR-0030,
AUTHOR = {Henning Makholm and J. B. Wells},
TITLE = {Type Inference and Principal Typings for Symmetric
Record Concatenation and Mixin Modules},
YEAR = 2005,
MONTH = MAR,
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
Sci.},
DATE = {2005-03-23},
HWUDATE = {2005-03-29},
NUMBER = {HW-MACS-TR-0030},
DISABLEDPDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0030.pdf},
DISABLEDPDFREMARK = {this is an obsolete presentation, so we don't want it on the web page},
CHURCHREPORT = {no},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Mak+Wel:ICFP-2005,
AUTHOR = {Henning Makholm and J. B. Wells},
TITLE = {Type Inference, Principal Typings, and
Let-Polymorphism for First-Class Mixin Modules},
CROSSREF = {ICFP2005},
CHURCHREPORT = {yes},
DARTREPORT = {yes},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Makholm+Wells:Type-Inference,-Principal-Typings,-and-Let-Polymorphism-for-First-Class-Mixin-Modules:ICFP-2005.pdf},
PAGES = {156--167},
ABSTRACT = {A \emph{mixin module} is a programming abstraction
that simultaneously generalizes
$\lambda$-abstractions, records, and mutually
recursive definitions. Although various mixin module
type systems have been developed, no one has
investigated \emph{principal typings} or developed
\emph{type inference} for first-class mixin modules,
nor has anyone added Milner's
\emph{let-polymorphism} to such a system.
\par
This paper proves that typability is NP-complete for
the naive approach followed by previous mixin module
type systems. Because a $\lambda$-calculus extended
with \emph{record concatenation} is a simple
restriction of our mixin module calculus, we also
prove the folk belief that typability is NP-complete
for the naive early type systems for record
concatenation.
\par
To allow feasible type inference, we present
\textsf{Martini}, a new system of \emph{simple
types} for mixin modules with \emph{principal
typings}. \textsf{Martini} is conceptually simple,
with no subtyping and a clean and balanced
separation between unification-based type inference
with type and row variables and constraint solving
for safety of linking and field extraction. We have
implemented a type inference algorithm and we prove
its complexity to be $O(n^2)$, or $O(n)$ given a
fixed bound on the number of field
labels. (Technically, there is also a factor of
$\alpha(n)$, but $\alpha(n)\leq 4$ for
$n<10^{10^{100}}$ (a ``googolplex'').) To prove the
complexity, we need to present an algorithm for
\emph{row unification} that may have been
implemented by others, but which we could not find
written down anywhere. Because \textsf{Martini} has
principal typings, we successfully extend it with
Milner's let-polymorphism.}
}
@INPROCEEDINGS{Haa+Wel:ESOP-2003,
ITRSPAPER = {yes},
AUTHOR = {Christian Haack and J. B. Wells},
TITLE = {Type Error Slicing in Implicitly Typed Higher-Order
Languages},
YEAR = 2003,
CROSSREF = {ESOP2003},
PAGES = {284--301},
CHURCHREPORT = {yes},
NOTE = {Superseded by \cite{Haa+Wel:SCP-2004-v50}},
DARTREPORT = {yes},
XDARTREPORT = {not a DART paper, although its journal version is part of a deliverable},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Haack+Wells:Type-Error-Slicing-in-Implicitly-Typed-Higher-Order-Languages:ESOP-2003.pdf},
ABSTRACT = {Previous methods have generally identified the
location of a type error as a particular program
point or the program subtree rooted at that
point. We present a new approach that identifies the
location of a type error as a set of program
points (a \emph{slice}) all of which are necessary
for the type error. We describe algorithms for
finding minimal type error slices for implicitly typed
higher-order languages like Standard ML.}
}
@ARTICLE{Haa+Wel:SCP-2004-v50,
ITRSPAPER = {yes},
AUTHOR = {Christian Haack and J. B. Wells},
TITLE = {Type Error Slicing in Implicitly Typed Higher-Order
Languages},
JOURNAL = {Sci.\ Comput.\ Programming},
DARTREPORT = {yes},
VOLUME = 50,
PAGES = {189--224},
YEAR = 2004,
PDFTODO = {*** rename this file ***},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Haack+Wells:Type-Error-Slicing-in-Implicitly-Typed-Higher-Order-Languages:SCP-ta.pdf},
CHURCHREPORT = {yes},
NOTE = {Supersedes \cite{Haa+Wel:ESOP-2003}},
DOIHTTP = {http://dx.doi.org/10.1016/j.scico.2004.01.004},
DOI = {doi:10.1016/j.scico.2004.01.004},
ABSTRACT = {Previous methods have generally identified the
location of a type error as a particular program
point or the program subtree rooted at that
point. We present a new approach that identifies the
location of a type error as a set of program points
(a \emph{slice}) all of which are necessary for the
type error. We identify the criteria of
\emph{completeness} and \emph{minimality} for type
error slices. We discuss the advantages of complete
and minimal type error slices over previous methods
of presenting type errors. We present and prove the
correctness of algorithms for finding complete and
minimal type error slices for implicitly typed
higher-order languages like Standard~ML.}
}
@ARTICLE{Haa+Wel:SCP-2004-v50-no-supersedes-special-issue,
AUTHOR = {Christian Haack and J. B. Wells},
TITLE = {Type Error Slicing in Implicitly Typed Higher-Order
Languages},
JOURNAL = {Sci.\ Comput.\ Programming},
DARTREPORT = {yes},
VOLUME = 50,
PAGES = {189--224},
YEAR = 2004,
PDFTODO = {*** rename this file ***},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Haack+Wells:Type-Error-Slicing-in-Implicitly-Typed-Higher-Order-Languages:SCP-ta.pdf},
NOTE = {Special issue of best papers from ESOP '03},
DOIHTTP = {http://dx.doi.org/10.1016/j.scico.2004.01.004},
DOI = {doi:10.1016/j.scico.2004.01.004},
ABSTRACT = {Previous methods have generally identified the
location of a type error as a particular program
point or the program subtree rooted at that
point. We present a new approach that identifies the
location of a type error as a set of program points
(a \emph{slice}) all of which are necessary for the
type error. We identify the criteria of
\emph{completeness} and \emph{minimality} for type
error slices. We discuss the advantages of complete
and minimal type error slices over previous methods
of presenting type errors. We present and prove the
correctness of algorithms for finding complete and
minimal type error slices for implicitly typed
higher-order languages like Standard~ML.}
}
@INPROCEEDINGS{Kfo+Was+Wel:ITRS-2002,
ITRSPAPER = {yes},
AUTHOR = {Assaf J. Kfoury and Geoff Washburn and J. B. Wells},
TITLE = {Implementing Compositional Analysis Using
Intersection Types With Expansion Variables},
CROSSREF = {ITRS2002},
NOTEREMARK = {The note field is blank to suppress the note field from ITRS2002.},
NOTE = {},
DARTREPORT = {yes},
CHURCHREPORT = {yes},
NONEXISTENTDVI = {http://www.church-project.org/reports/electronic/Kfo+Was+Wel:ITRS-2002.dvi},
PDF = {http://www.church-project.org/reports/electronic/Kfo+Was+Wel:ITRS-2002.pdf},
ELSEVIERURLB = {http://www.elsevier.nl/gej-ng/31/29/23/125/51/show/Products/notes/index.htt},
ELSEVIERURLA = {http://www.elsevier.nl/locate/entcs/volume70.html},
ABSTRACT = {A program analysis is \emph{compositional} when the analysis
result for a particular program fragment is obtained solely from the
results for its immediate subfragments via some composition operator. This
means the subfragments can be analyzed independently in any order. Many
commonly used program analysis techniques (in particular, most abstract
interpretations and most uses of the Hindley/Milner type system) are not
compositional and require the entire text of a program for sound and
complete analysis. \par System I is a recent type system for the pure
$\lambda$-calculus with intersection types and the new technology of
expansion variables. System I supports compositional analysis because it
has the \emph{principal typings} property and an algorithm based on the new
technology of $\beta$-unification has been developed that finds these
principal typings. In addition, for each natural number $k$, typability in
the rank-$k$ restriction of System I is decidable, so a complete and
terminating analysis algorithm exists for the rank-$k$ restriction. \par
This paper presents new understanding that has been gained from working
with multiple implementations of System I and $\beta$-unification-based
analysis algorithms. The previous literature on System I presented the
type system in a way that helped in proving its more important theoretical
properties, but was not as easy for implementers to follow as it could be.
This paper provides a presentation of many aspects of System I that should
be clearer as well as a discussion of important implementation issues.}
}
@INPROCEEDINGS{Car+Pol+Wel+Kfo:ESOP-2004,
ITRSPAPER = {yes},
CHURCHREPORT = {yes},
DARTREPORT = {yes},
AUTHOR = {S{\'e}bastien Carlier and Jeff Polakow and
J. B. Wells and A. J. Kfoury},
TITLE = {{S}ystem {E}: Expansion Variables for Flexible Typing
with Linear and Non-linear Types and Intersection
Types},
CROSSREF = {ESOP2004},
PAGES = {294--309},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Polakow+Wells+Kfoury:System-E:ESOP-2004.pdf},
ALTPDF = {http://www.macs.hw.ac.uk/DART/reports/D2.3/CPWK04.pdf},
ABSTRACT = {Types are often used to control and analyze computer
programs. Intersection types give a type system
great flexibility, but have been difficult to
implement. The $!$ operator, used to distinguish
between linear and non-linear types, has good
potential for improving tracking of resource usage,
but has not been as flexible as one might want and
has been difficult to use in compositional
analysis. We introduce System~E, a type system with
expansion variables, linear intersection types, and
the $!$ type constructor for creating non-linear
types. System~E is designed for maximum flexibility
in automatic type inference and for ease of
automatic manipulation of type
information. Expansion variables allow postponing
the choice of which typing rules to use until later
constraint solving gives enough information to allow
making a good choice. System~E removes many
limitations and technical difficulties that
expansion variables had in the earlier System~I and
extends expansion variables to work with $!$ in
addition to the intersection type constructor. We
present subject reduction results for call-by-need
evaluation and discuss approaches for implementing
program analysis in System~E.}
}
@TECHREPORT{Car+Wel:TIEV-2004,
ITRSPAPER = {no},
CHURCHREPORT = {no},
DARTREPORT = {yes},
AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
TITLE = {Type Inference with Expansion Variables and
Intersection Types in {S}ystem~{E} and an Exact
Correspondence with $\beta$-Reduction},
DISABLEDPDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0012.pdf},
XPDF = {http://www.macs.hw.ac.uk/DART/reports/D2.3/CW04.pdf},
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\ Sci.},
YEAR = 2004,
NUMBER = {HW-MACS-TR-0012},
MONTH = JAN,
NOTE = {Completely superseded by \cite{Car+Wel:PPDP-2004}},
REMARK = {Don't cite this anymore! It is completely obsolete.
It only remains because it is officially reported
work on the DART grant.},
ABSTRACT = {System~E is a recently designed type system for the
$\lambda$-calculus with intersection types and
\emph{expansion variables}. During automatic type
inference, expansion variables allow postponing
decisions about which non-syntax-driven typing rules
to use until the right information is available and
allow the choices to be implemented via
substitution.
\par
This paper shows how expansion variables enable a
unification-based automatic type inference algorithm
for System E that finds a typing for every
$\beta$-normalizable $\lambda$-term. We have
implemented and tested our algorithm and made our
implementation publicly available. We show that each
step of our unification algorithm corresponds to
exactly one $\beta$-reduction step, and \emph{vice
versa}. This formally verifies and makes precise a
correspondence between type inference and
$\beta$-reduction that before was only known
informally at an intuitive level and only among
those who work with intersection types.}
}
@INPROCEEDINGS{Car+Wel:PPDP-2004,
ITRSPAPER = {yes},
CHURCHREPORT = {yes},
DARTREPORT = {yes},
AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
TITLE = {Type Inference with Expansion Variables and
Intersection Types in {S}ystem~{E} and an Exact
Correspondence with $\beta$-Reduction},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Wells:Type-Inference-with-Expansion-Variables-and-Intersection-Types-in-System-E-and-an-Exact-Correspondence-with-Beta-Reduction:PPDP-2004.pdf},
CROSSREF = {PPDP2004},
XPAGES = {132--143},
NOTE = {Completely supersedes \cite{Car+Wel:TIEV-2004}},
ABSTRACT = {System~E is a recently designed type system for the
$\lambda$-calculus with intersection types and
\emph{expansion variables}. During automatic type
inference, expansion variables allow postponing
decisions about which non-syntax-driven typing rules
to use until the right information is available and
allow implementing the choices via substitution.
\par
This paper uses expansion variables in a
unification-based automatic type inference algorithm
for System~E that succeeds for every
$\beta$-normalizable $\lambda$-term. We have
implemented and tested our algorithm and released
our implementation publicly. Each step of our
unification algorithm corresponds to exactly one
$\beta$-reduction step, and \emph{vice versa}. This
formally verifies and makes precise a step-for-step
correspondence between type inference and
$\beta$-reduction. This also shows that type
inference with intersection types and expansion
variables can, in effect, carry out an arbitrary
amount of partial evaluation of the program being
analyzed.}
}
@INPROCEEDINGS{Car+Wel:ITRS-2004,
ITRSPAPER = {yes},
DARTREPORT = {yes},
DOI = {doi:10.1016/j.entcs.2005.03.026},
URL = {http://dx.doi.org/10.1016/j.entcs.2005.03.026},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Wells:Expansion:ITRS-2004.pdf},
AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
TITLE = {Expansion: the Crucial Mechanism for Type Inference
with Intersection Types: {A} Survey and Explanation},
PAGES = {173--202},
CROSSREF = {ITRS2004},
ABSTRACT = {The operation of \emph{expansion} on typings was
introduced at the end of the 1970s by Coppo, Dezani,
and Venneri for reasoning about the possible typings
of a term when using intersection types. Until
recently, it has remained somewhat mysterious and
unfamiliar, even though it is essential for carrying
out \emph{compositional} type inference. The
fundamental idea of expansion is to be able to
calculate the effect on the final judgement of a
typing derivation of inserting a use of the
intersection-introduction typing rule at some
(possibly deeply nested) position, without actually
needing to build the new derivation. Recently, we
have improved on this by introducing \emph{expansion
variables} (E-variables), which make the calculation
straightforward and understandable. E-variables
make it easy to postpone choices of which typing
rules to use until later constraint solving gives
enough information to allow making a good choice.
Expansion can also be done for type constructors
other than intersection, such as the ! of Linear
Logic, and E-variables make this easy. There are no
significant new technical results in this paper;
instead this paper surveys and explains the
technical results of a quarter of a century of work
on expansion.}
}
@TECHREPORT{Car+Wel:expansion-TR-2005,
ITRSPAPER = {no},
CHURCHREPORT = {no},
DARTREPORT = {yes},
AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
TITLE = {Expansion: the Crucial Mechanism for Type Inference
with Intersection Types: Survey and Explanation},
DISABLEDPDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0029.pdf},
XPDF = {http://www.macs.hw.ac.uk/DART/reports/D5.3/CW05.pdf},
INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\ Sci.},
YEAR = 2005,
NUMBER = {HW-MACS-TR-0029},
MONTH = FEB,
HWU-DATE = {2005-03-18}
}
@INPROCEEDINGS{Cop-DLag-Ron:EALCBV-04,
AUTHOR = {P. Coppola and U. Dal Lago and Ronchi Della Rocca,
Simona},
TITLE = {Elementary Affine Logic and the Call by Value Lambda
Calculus},
PDF = {http://www.di.unito.it/~ronchi/papers/llcbv.pdf},
YEAR = 2005,
PAGES = {131--145},
EDITOR = {P. Urzyczyn},
BOOKTITLE = {Typed Lambda Calculi and Applications, 7th
International Conference, TLCA 2005, Nara, Japan,
April 21-23, 2005, Proceedings},
PUBLISHER = {Springer-Verlag},
SERIES = {LNCS},
VOLUME = 3461,
ABSTRACT = {Light and elementary linear logics have been
introduced as logical systems enjoying quite
remarkable normalization properties. Designing a
type assignment system for pure lambda calculus from
these logics, however, is problematic. In this
paper, we show that shifting from usual call-by-name
to call-by-value lambda calculus allows to regain
strong connections with the underlying logic. We
will do this in the context of Elementary Affine
Logic (EAL), designing a type system in natural
deduction style assigning EAL formulae to lambda
terms.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Cop+Ron:2002,
AUTHOR = {P. Coppola and Ronchi Della Rocca, Simona},
TITLE = {{P}rincipal {T}yping in {E}lementary {A}ffine
{L}ogic},
EDITOR = {Martin Hofmann},
BOOKTITLE = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
PAGES = {90-104},
VOLUME = 2701,
YEAR = 2003,
ABSTRACT = {Elementary Affine Logic (EAL) is a variant of the
Linear Logic
characterizing the computational power of the elementary bounded
Turing 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 \emph{type schemata}, from which all and only
its typings
can be derived, through suitable operations},
PDF = {http://www.di.unito.it/~ronchi/papers/EA-typing.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Cop+Ron:LL-2002,
AUTHOR = {P. Coppola and Ronchi Della Rocca, Simona},
TITLE = {{P}rincipal {T}yping in {E}lementary {A}ffine
{L}ogic},
EDITOR = {Martin Hofmann},
BOOKTITLE = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
PAGES = {90-104},
VOLUME = 2701,
YEAR = 2003,
ABSTRACT = {Elementary Affine Logic (EAL) is a variant of the
Linear Logic
characterizing the computational power of the elementary bounded
Turing 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 \emph{type schemata}, from which all and only
its typings
can be derived, through suitable operations},
PDF = {http://www.di.unito.it/~ronchi/papers/EA-typing.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Ronchi:ITRS-2002,
ITRSPAPER = {yes},
AUTHOR = {Ronchi Della Rocca, Simona},
TITLE = {Intersection Typed lambda-calculus},
BOOKTITLE = {ITRS 2002},
YEAR = {2002},
PUBLISHER = {Elsevier},
SERIES = {ENTCS},
VOLUME = {70.1},
PAGES = {},
PDF = {http://www.di.unito.it/~ronchi/papers/ronchi-itrs02.pdf},
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.},
DARTREPORT = {yes}
}
@ARTICLE{Cop+Ron:FI-2005,
AUTHOR = {P. Coppola and Ronchi Della Rocca, Simona},
TITLE = {Principal Typing for Lambda Calculus in Elementary Affine Logic},
JOURNAL = {Fundamenta Informaticae},
YEAR = 2005,
VOLUME = 65,
NUMBER = {1-2},
PAGES = {87-112},
ABSTRACT = {Elementary Affine Logic (EAL) is a variant of Linear Logic characterizing
the computational power of the elementary bounded Turing machines.
The EAL Type Inference problem is the problem of automatically assigning
to terms of l-calculus EAL formulas as types.
This problem, restricted to the propositional fragment of EAL,
is proved to be decidable, and an algorithm is shown, building, for every l-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.},
PDF = {http://www.di.unito.it/~ronchi/papers/EA-typingFI.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Coppola+Ronchi:TLCA-2003,
AUTHOR = {P. Coppola and Ronchi Della Rocca, Simona},
TITLE = {{P}rincipal {T}yping in {E}lementary {A}ffine
{L}ogic},
EDITOR = {Martin Hofmann},
BOOKTITLE = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
PAGES = {90-104},
VOLUME = 2701,
YEAR = 2003,
ABSTRACT = {Elementary Affine Logic (EAL) is a variant of the
Linear Logic
characterizing the computational power of the elementary bounded
Turing 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 \emph{type schemata}, from which all and only
its typings
can be derived, through suitable operations},
PDF = {http://www.di.unito.it/~ronchi/papers/EA-typing.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{And+Dro:BabyJ-2002,
AUTHOR = {Christopher Anderson and Sophia Drossopoulou},
TITLE = {{BabyJ} - From Object Based to Class Based
Programming via Types},
BOOKTITLE = {WOOD '03},
YEAR = {2003},
SERIES = {ENTCS},
VOLUME = {82},
PAGES = {},
PUBLISHER = {Elsevier},
PDF = {http://www.binarylord.com/work/babyj.pdf},
ABSTRACT = { The popularity of object based languages has risen dramatically in recent
years, owing to their use as scripts in HTML pages, or for interfacing
with
databases. A characteristic of these languages is interpretation and weak
typing. Weak typing allows rapid prototyping but also runtime type errors.
Therefore, it is desirable at a later development stage to have some
assurances that your program will not go wrong.
\par
Class based programming languages usually have static typing and thus
give more robust programs. However, owing to the rigidity of the type
system prototyping can be difficult.
\par
We propose a language, BabyJ, that combines the benefits of object
based programming and types. BabyJ allows rapid ``typeless''
development and also gives the programmer the opportunity to incrementally
annotate the program with type information. Once fully typed, a BabyJ
program can be converted to an equivalent Java program, that can be
developed further.},
DARTREPORT = {yes}
}
@UNPUBLISHED{And+Dro:delta-2003,
AUTHOR = {Christopher Anderson and Sophia Drossopoulou},
TITLE = {$\delta$ - an imperative object based calculus with delegation, for unanticipated software evolution},
YEAR = {2003},
NOTE = {Submitted for publication},
PDF = {http://www.binarylord.com/work/esopdelta.pdf},
ABSTRACT = {Unanticipated software evolution requires software needs to
evolve at a very late stage. We argue that the main programming
language ingredients necessary to support unanticipated software
evolution are objects whose methods may change at runtime, whose
members may be augmented, and which may delegate behaviour to
other objects at run-time, in an imperative setting.
\par
We suggest $\delta$, a formal calculus that supports all the above.
We show key features of $\delta$ though examples and how these
support unanticipated software evolution.
\par
This work is an extension of work presented at USE2002.},
DARTREPORT = {yes}
}
@UNPUBLISHED{And+Dro:delta-2002,
AUTHOR = {Christopher Anderson and Sophia Drossopoulou},
TITLE = {$\delta$ - an imperative object based calculus with
delegation},
YEAR = {2002},
NOTE = {Presented at the workshop USE in 2002, Malaga},
PDF = {http://www.binarylord.com/work/delta.pdf},
ABSTRACT = {Object based, imperative languages with delegation
(eg SELF) support
exploratory programming: composition of objects, sharing of
attributes
and modification of objects' behaviour at run-time are easily
expressible.
Delegation allows objects to delegate execution of methods to
other objects
and to adapt delegated behaviour by overriding of method
definitions. These
features allow for creation of very flexible
programs that can accomodate requirement changes at a very late
stage.
\par
Programming language design and understanding has generally
benefited from formal models of programming languages. Such
models, of
course, tend to focus on the essential features of the
particular
language, making it possible to highlighting design alternatives
and compare
them. Models for object based languages have already been
developed in the
90's, but these models do not directly express imperative
delegation.
\par
We argue that no calculi so far developed fully express the
essence of such languages. We give a simple intuitive calculus
for
imperative object based delegation. We start with $\delta^{-}$, an
imperative
object based calculus, and demonstrate its use through examples.
$\delta^{-}$ is
similar to the first order imperative Abadi Cardelli calculus,
though
simpler in some sense. We prove a correspondence theorem. We
then present
$\delta$, which extends $\delta^{-}$ through explicit delegation;
$\delta$\ allows an object to specify explicitly to which
objects it wants
to delegate. We show key features of $\delta$\ through examples},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Buc+Dro:ftfjp04,
AUTHOR = {Alex Buckley and Sophia Drossopoulou},
TITLE = {Flexible Dynamic Linking},
BOOKTITLE = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)},
YEAR = {2004},
MONTH = {June},
ADDRESS = {Oslo, Norway},
URL = {http://www.cs.ru.nl/~erikpoll/ftfjp/2004.html},
ABSTRACT = {Dynamic linking, as in Java and C#, allows users to execute the most recent versions of software without re-compilation or re-linking. Dynamic linking is guided by type names stored in the bytecode.
In current dynamic linking schemes, these type names are hard-coded into the bytecode. Thus, the bytecode reflects the compilation environment that produced it. However, the compilation environment need not be the same as the execution environment: a class may be replaced by one that offers the "same" services but has a different name. Such changes are not supported by current linking schemes.
We suggest a more flexible approach to dynamic linking, where bytecode contains type variables rather than types, and where these type variables are substituted during execution. We develop a non-deterministic system that allows type variable substitution at many different points, and sketch a proof of soundness.
},
PDF = {http://www.macs.hw.ac.uk/DART/reports/D5.3/BD04.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Buc+Mur+Eis+Dro:bytecode05,
AUTHOR = {Alex Buckley and Michelle Murray and Susan Eisenbach and Sophia Drossopoulou},
TITLE = {Flexible Bytecode for Linking in .NET},
BOOKTITLE = {ETAPS Workshop BYTECODE},
YEAR = {2005},
MONTH = {March},
ADDRESS = {Edinburgh, UK},
URL = {http://slurp.doc.ic.ac.uk/pubs.html},
PDF = {http://slurp.doc.ic.ac.uk/pubs/flexiblebytecodefordotnet-bytecode05.pdf},
ABSTRACT = {
Dynamic linking in modern execution environments like .NET is considerably more sophisticated than in the days of C shared libraries on UNIX. One aspect of this sophistication is that .NET assemblies embed type information about dynamically linked resources.
This type information implicitly represents compile-time assumptions about the resources available at run-time. However, at run-time, different resources may actually be available. For example, the execution environment on a mobile phone might provide fewer, simpler classes than on a desktop PC.
We have designed and implemented a "flexible" dynamic linking scheme that supports the run-time selection of .NET assemblies and classes. This enables a regime of "compile once, run anywhere". We describe the scheme's integration with the .NET linking infrastructure, review important design decisions and report on experiences with the "Rotor" shared source version of .NET.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Jol+Dro+And+Ost:ftfjp04,
AUTHOR = {Paul Jolly and Sophia Drossopoulou and Christopher Anderson and Klaus Ostermann},
TITLE = {Simple Dependent Types: Concord},
BOOKTITLE = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)},
YEAR = {2004},
MONTH = {June},
ADDRESS = {Oslo, Norway},
URL = {http://myitcv.org.uk/papers/concord04.html},
PDF = {http://myitcv.org.uk/papers/files/concord_workshop.pdf},
ABSTRACT = {We suggest a simple model for a restricted form of dependent types in object oriented languages, whereby classes belong to groups and dependency is introduced via intra-group references using the MyGrp keyword. We show how our approach can code well-known examples from the literature, present the formal model and outline soundness of the type system.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Lag+Mar+Rov:TYPES-2003,
AUTHOR = {U. Dal Lago and S. Martini and L. Roversi},
TITLE = {Higher-Order Linear Ramified Recurrence},
BOOKTITLE = {Proceedings of TYPES'04},
VOLUME = {3085},
SERIES = {LNCS},
PAGES = {178 -- 193},
PUBLISHER = {Springer-Verlag},
MONTH = DEC,
YEAR = 2004,
DISABLEDDOCUMENTURL = {http://www.di.unito.it/~rover/PAPERS/TYPES03.html},
PDF = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2004-TYPES/DalLagoMartiniRoversi2004TYPES.ps.gz},
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},
DARTREPORT = {yes}
}
@UNPUBLISHED{Roversi:miniecole-2003,
AUTHOR = {L. Roversi},
TITLE = {An Introduction to Intuitionistic Light Affine Logic},
NOTE = {Lecture notes -- Mini (Doctoral) School Chamb\'ery/Turin of
Theoretical Computer Science},
MONTH = {Jan},
YEAR = {2003},
PDF = {http://www.di.unito.it/~rover/TEACHING/aussois.ps.gz},
DOCUMENTURL = {http://www.di.unito.it/~rover/TEACHING/aussois-03.html},
DARTREPORT = {yes},
ABSTRACT = {These notes use Light Affine Logic to introduce the basic principles
that can be exploited, inside Linear Logic, to control the complexity of
the cut elimination}
}
@UNPUBLISHED{Roversi:2002,
AUTHOR = {L. Roversi},
TITLE = {{F}lexible {A}ffine {L}ight {L}ogic},
YEAR = {2002},
NOTE = {Submitted to a journal
-- a preliminary version has been
presented at the workshop ``LL---Linear Logic'',
affiliated to FLoC'02, Copenhagen},
ABSTRACT = {At least two approaches to machine-independent
characterizations of polynomially costing computations exist.
One is purely proof-theoretic. It has been developed by
introducing Light linear logic, and it is based on a careful
control of the expressiveness of the logical rule contraction.
The other approach is recursion-theoretic. It exists in various
forms. Every of them is based essentially on some restrictions
of both a recursion and a composition scheme, with of without
the
help of some typing discipline. Flexible Affine Light Logic
(FALL)
allows to bridge the two approaches. FALL derives from Light
linear
logic. It admits a polynomially costing normalization strategy.
Moreover, there is an inductive embedding of the full system BC
into
FALL, BC being a recursive-theoretic characterization of
poly-time,
by Bellantoni and Cook. So, FALL is expressive enough to
represent
all the feasible computations. The distinguishing feature of
FALL is
that it is a proof-theoretic system that both embodies the quite
restrictive structural constraints a` la Linear logic to control
the
reduction complexity, and keeps such constraints flexible enough
to encode, and simulate, the more programming-oriented terms of
BC.
The paper fully formalizes the structure, and the properties of
FALL.
It also shows the details of the relation with BC, so opening
the
possibility for various comparisons of one approach to feasible
computations vs. the other. },
DARTREPORT = {yes},
DUP = {***duplicate of Roversi-FALL-2001***to be fixed***}
}
@UNPUBLISHED{Pao:IC-05,
AUTHOR = {Paolini, Luca},
TITLE = {A stable programmming language},
NOTE = {To appear in Information and Computation},
ABSTRACT = {It is well-known that stable functions
do not produce a fully abstract model with respect to the usual operational semantics of PCF.
This fact is related to the existence of stable ``parallel'' functions
and to the existence of some stable functions not monotone with respect to the extensional order,
which cannot be represented by programs of PCF.
In this paper, it is proposed an extension of PCF with two additional operators
already appeared in literature, for which a constructive ``operational description'' is formalized.
It is proved that this extension is
complete for defining the finite elements of stable model.
Hence, it follows that stable model is fully abstract model for the extended language.},
PDF = {http://www.unifi.it/eatcs/award/PaoliniThesis.pdf},
YEAR = 2005,
DARTREPORT = {yes}
}
@ARTICLE{ro-pa-03,
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. },
PDF = {http://www.di.unito.it/~ronchi/papers/cr.pdf},
POSTSCRIPT = {http://www.di.unito.it/~ronchi/papers/cr.ps},
YEAR = 2004,
DARTREPORT = {yes}
}
@INPROCEEDINGS{Anc+Lag+Zuc:ECOOP-2002,
AUTHOR = {D. Ancona and G. Lagorio and E. Zucca},
TITLE = {A Formal Framework for {J}ava Separate Compilation},
EDITOR = {B. Magnusson},
PAGES = {609--635},
CROSSREF = {ECOOP2002},
DARTREPORT = {yes},
ABSTRACT = {We define a formal notion, called \emph{compilation
schema}, suitable for specifying different possibilities for
performing the overall process of Java compilation, which
includes typechecking of source fragments with generation of
corresponding binary code, typechecking of binary fragments,
extraction of type information from fragments and definition of
dependencies among them. We consider three compilation schemata
of interest for Java, that is, \emph{minimal}, \emph{SDK} and
\emph{safe}, which correspond to a minimal set of checks, the
checks performed by the SDK implementation, and all the checks
needed to prevent run-time linkage errors, respectively. In
order to demonstrate our approach, we define a kernel model for
Java separate compilation and execution, consisting in a small
Java subset, and a simple corresponding binary language for
which we provide an operational semantics including run-time
verification. We define a safe compilation schema for this
language and formally prove type safety.},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/AncLagZuc-ECOOP2002.pdf}
}
@INPROCEEDINGS{Anc+Lag+Zuc:PPDP-2002,
AUTHOR = {D. Ancona and G. Lagorio and E. Zucca},
TITLE = {True Separate Compilation of {J}ava Classes},
CROSSREF = {PPDP2002},
DARTREPORT = {yes},
ABSTRACT = {We define a type system modeling true separate
compilation for a small but significant Java subset, in the
sense that a single class declaration can be intra-checked
(following the Cardelli's terminology) and compiled providing a
minimal set of type requirements on missing classes. These
requirements are specified by a local type environment
associated with each single class, while in the existing formal
definitions of the Java type system classes are typed in a
global type environment containing all the type information on a
closed program. We also provide formal rules for static
inter-checking and relate our approach with compilation of
closed programs, by proving that we get the same results.},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/AncLagZuc-PPDP2002.pdf}
}
@ARTICLE{Anc+Lag+Zuc:TOPLAS-2003,
AUTHOR = {D.~Ancona and G.~Lagorio and E.~Zucca},
TITLE = {{Jam}---designing a {Java} extension with mixins},
JOURNAL = {ACM Transactions on Programming Languages and Systems},
VOLUME = {25},
NUMBER = {5},
PAGES = {641--712},
MONTH = {September},
YEAR = {2003},
DARTREPORT = {yes},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/AncLagZuc-TOPLAS2003.pdf},
ABSTRACT = {In this paper we present Jam, an extension of the Java language
supporting mixins, that is, parametric heir classes. A mixin declaration
in Jam is similar
to a Java heir class declaration, except that it does not extend a
fixed parent class, but simply specifies the set of fields and methods
a generic parent should provide. In this way, the same mixin can be
instantiated on
many parent classes, producing different heirs, thus avoiding code
duplication and largely improving modularity and reuse. Moreover, as
happens for classes and interfaces, mixin names are reference types, and
all the classes
obtained by instantiating the same mixin are considered subtypes of the
corresponding type, hence can be handled in a uniform way through the
common interface. This possibility allows a programming style where
different ingredients are ``mixed'' together in defining a class; this
paradigm is somewhat similar to that based on multiple inheritance, but
avoids its complication.
The language has been designed with the main objective in mind to obtain,
rather than a new
theoretical language, a working and smooth extension of Java.
That means, on the design side, that we have faced the challenging problem
of integrating the
Java overall principles and complex type system with this new
notion; on the implementation side, that we have developed a Jam to
Java translator which makes Jam sources executable on every Java Virtual
Machine. }
}
@INPROCEEDINGS{Anc+Lag+Zuc:FTFjP-2005,
AUTHOR = {D.~Ancona and G.~Lagorio and E.~Zucca},
TITLE = {Smart Modules for {J}ava-like Languages},
BOOKTITLE = {ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2005)},
ADDRESS = {Glasgow, Scotland},
INSTITUTION = {Dipartimento di Informatica e Scienze dell'Infomazione, Universit\`a di Genova},
ABSTRACT = {
We present SmartJavaMod, a language of mixin modules supporting
\emph{compositional compilation}, and constructed on
top of the Java language. More in detail, this means that basic modules are
collections of Java classes
which can be typechecked in isolation, inferring constraints on missing classes and
allowing safe reuse of the module in as many contexts as possible.
Furthermore, it is possible to write
structured module expressions
by means of a set of module operators, and a type system at the
module level ensures type safety, in the sense that we can always reduce a module
expression to a well-formed collection of Java classes.
What we obtain is a module language
which is extremely flexible and
allows the encoding (without any need of enriching the core level, that is,
the Java language) of a variety of constructs supporting software reuse and extensibility.
},
YEAR = 2005,
MONTH = JUL,
DARTREPORT = {yes},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/AncLagZuc-FTfJP05.pdf}
}
@INPROCEEDINGS{Lag:ICTCS-2003,
AUTHOR = {G. Lagorio},
TITLE = {Towards a Smart Compilation Manager for {J}ava},
MONTH = OCT,
PAGES = {302--315},
CROSSREF = {ICTCS2003},
ABSTRACT = {It is often infeasible to recompile all the sources an application consists of each time a change is made.
Yet, a recompilation strategy which does not guarantee the same outcome of an entire recompilation is not useful:
why wasting time in debugging a program (a set of .class files in the Java case) which might behave differently from the program
obtained recompiling all the sources from scratch?
We say that a compilation strategy is sound if it recompiles, besides the changed sources, all the unchanged sources whose new binary, produced by the overall recompilation, would differ from the existing one (if any) and all the sources for which the recompilation would be undefined: indeed, when the entire compilation fails, so should do the partial recompilation.
We say that a compilation strategy is minimal if it never recompiles an unchanged source whose new binary would be equal to the existing one.
In this paper we present a compilation strategy for a substantial subset of Java which is proved to be sound and minimal.},
DARTREPORT = {yes},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/Lag-ICTCS2003.pdf}
}
@INPROCEEDINGS{Lag:SAC-2004,
AUTHOR = {G. Lagorio},
TITLE = {Another step towards a smart compilation manager for {J}ava},
CROSSREF = {SAC-2004},
PAGES = {1275--1280},
MONTH = MAR,
ABSTRACT = {In a recent work we have proposed a compilation strategy (that is, a way to decide which unchanged sources have to be
recompiled) for a substantial subset of Java which has been shown to be sound and minimal.
That is, an unchanged source is recompiled if and only if its recompilation produces a different binary or an error.
However, that model does not handle two features of Java, namely, compile-time constant fields (static final fields initialized by a compile-time constant of a primitive type or String) and unreachable code, which turn out to be troublesome for
having a sound and minimal compilation strategy.
To our best knowledge these two features, probably because of their low-level nature,
have been omitted in all models of Java separate compilation written so far.
Yet, a compilation strategy for full Java has to deal with them.
Thus, in this paper we analyze the implications of
handling compile-time constant fields and unreachable code, and
extend our previous model in order to handle these two features as well.},
DARTREPORT = {yes},
PDF = {http://www.disi.unige.it/person/LagorioG/papers/Lag-SAC2004.pdf},
NOTE = {In OOPS track}
}
@INPROCEEDINGS{Anc+Lag:FTfJP03,
AUTHOR = {D.~Ancona and G.~Lagorio},
TITLE = {Stronger Typings for Separate Compilation of {J}ava-like Languages (Extended Abstract)},
YEAR = {2003},
MONTH = {July},
BOOKTITLE = {Fifth Workshop on Formal Techniques for Java Programs},
DOCUMENTURL = {http://www.cs.ru.nl/~erikpoll/ftfjp/},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/AncLag-FTfJP03.pdf},
DARTREPORT = {yes},
ABSTRACT = {
We define a formal system supporting
separate compilation for a small but significant Java-like
language.
This system permits to derive typings which are
stronger than those of the standard type systems
for Java, by introducing the notions of \emph{local type assumption}
and \emph{entailment of type environments}. The former
allows the user to specify weaker requirements on the source fragments
which need to be compiled in isolation, whereas the latter
syntactically captures the concept of stronger type environment.
One of the most important advantages of this approach
consists in a better support for selective recompilation;
indeed, based on the formal system, it is possible to
define an algorithm able to avoid the unnecessary recompilation steps
which are usually performed by the Java compilers.
Finally, we show how the whole system could be effectively
implemented in order to support true separate compilation.}
}
@ARTICLE{Anc+Lag:STSCJL-03-12,
AUTHOR = {D. Ancona and G. Lagorio},
TITLE = {Stronger Typings for Separate Compilation of {J}ava-like Languages},
JOURNAL = {Journal of Object Technology},
YEAR = 2004,
VOLUME = 3,
NUMBER = 6,
PUBLISHER = {Chair of Software Engineering (ETH Zurich)},
NOTE = {Extended version of \cite{Anc+Lag:FTfJP03}},
PDF = {http://www.jot.fm/issues/issue_2004_06/article1.pdf},
DARTREPORT = {yes},
ABSTRACT = {We define a formal system supporting
separate compilation for a small but significant Java-like
language.
This system permits to derive typings which are
stronger than those of the standard type systems
for Java, by introducing the notions of \emph{local type assumption}
and \emph{entailment of type environments}. The former
allows the user to specify weaker requirements on the source fragments
which need to be compiled in isolation, whereas the latter
syntactically captures the concept of stronger type environment.
One of the most important advantages of this approach
consists in a better support for selective recompilation;
indeed, based on the formal system, it is possible to
define an algorithm able to avoid the unnecessary recompilation steps
which are usually performed by the Java compilers.
Finally, we show how the whole system could be effectively
implemented in order to support true separate compilation.
}
}
@INPROCEEDINGS{Smi+Dro-2003a,
AUTHOR = {Matthew Smith and Sophia Drossopoulou},
TITLE = {Cheaper Reasoning with Ownership Types},
YEAR = 2003,
ABSTRACT = {We use ownership types to facilitate program
verification. Namely, an assertion that has been
established for a part of the heap which is
unaffected by some execution will still hold after
this execution. We use ownership and effects, and
extend them to assertions to be able to make the
judgement as to which executions do not affect which
assertions. We describe the ideas in terms of an
example, and outline the formal system.},
BOOKTITLE = {ECOOP 2003 International Workshop on Aliasing and
Confinement},
PDF = {http://slurp.doc.ic.ac.uk/pubs/cheaperreasoning-iwaco03.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Smi+Dro:FTJLP-2003,
AUTHOR = {Matthew Smith and Sophia Drossopoulou},
TITLE = {Inner Classes visit Aliasing},
YEAR = 2003,
BOOKTITLE = {ECOOP 2003 Workshop on Formal Techniques for Java-like
Programming},
PDF = {http://www.cs.ru.nl/~erikpoll/ftfjp/2003.html},
ABSTRACT = { Inner classes appear nested within class
definitions. They may access any members of the
classes in which they are contained. The interplay
between inner classes, aliasing and subclasses can
make resolution of such accesses intricate. We offer
a succinct model for member classes, in which we
highlight these intricacies and we prove
soundness. },
DARTREPORT = {yes}
}
@INPROCEEDINGS{Dro+Eis-2003,
AUTHOR = {Sophia Drossopoulou and Susan Eisenbach},
TITLE = {Flexible, Source level dynamic Linking and re-Linking},
YEAR = {2003},
ABSTRACT = {
Dynamic linking was introduced into programming languages to support
implicit linking of the newest version of libraries.
Partially linked code links further code on the
fly, as needed, and thus, most recent updates are
automatically available to end-users, without
the requirement of further compilations or re-linking.
The remit has recently been
extended, to support requirements from unanticipated
software evolution,
whereby code may need to be {\em updated}
{\em during} program execution.
To address such requirements, new features
of the JVM allow the replacement
of a class by a class of the same signature,
as a ``fix-and-continue'' feature
% \cite{hotSwap}, while in \cite{hicksDyn}
dynamic software updates support
type safe dynamic reloading of code whose type may have changed,
while the system is running.
% Also, \cite{Bier} suggest dynamic linking of modules, with the support
% of multiple versions of the same module.
% Finally, \cite{dynLinkGenova} suggest a calculus for dynamic
% linking independently of the programming language and environment.
We present the semantics for a
high level language similar to Java or
C\#
In contrast to earlier
formalizations of dynamic linking % \cite{load,flexiDynLink},
our model is purely at source language level.
Namely, although dynamic linking is
usually described at a ``low level'' % \cite{javaTwo},
in terms of generated *.class files,
its effects are visible to the source language programmer.% , as shown
% \eg through
% a sequence of examples in -\cite{dynexamplewebpage,sueExample}.
This is why, in our view, an explanation at source language level
is very important. In order to simplify the exposition,
we do not
deal with overloading or field shadowing.
In more detail, the model we suggest allows dynamic
linking at a very fine grain:
(1) Method signatures may be loaded before
verification of their corresponding bodies,
(2)
Method bodies need be verified only before execution%
% \footnote{This is
% similar to \CSharp dynamic linking.},
(3)
Classes may be loaded before their fields/methods,
(4)
Classes, methods and fields may be loaded ``piecemeal'',
(5)
Classes, methods, and fields may be removed, if not needed,
(6) Method bodies may be replaced.
},
BOOKTITLE = {ECOOP 2003 Workshop on Formal Techniques for Java
Programs},
PDF = {http://www.cs.ru.nl/~erikpoll/ftfjp/2003/14.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Dro+Lag+Eis-2003,
AUTHOR = {Sophia Drossopoulou and Giovanni Lagorio and Susan Eisenbach},
CROSSREF = {ESOP2003},
TITLE = {Flexible Models for Dynamic Linking},
YEAR = {2003},
ABSTRACT = {
Dynamic linking supports flexible code deployment: partially
linked code links further code on the fly, as needed;
and thus, end-users receive updates automatically.
On the down side, each program run may link
different versions of the same code,
possibly causing subtle errors which mystify end-users.
Dynamic linking in Java and C\# are similar: The same linking
phases are involved, soundness is based on similar ideas, and
executions which do not throw linking errors give the same result.
They are, however, not identical: the linking phases are combined
differently, and take place in different order. Thus, linking
errors may be detected at different times in Java and C\#.
We develop a non-deterministic model, which
includes the behaviour of Java and C\#. The non-determinism
allows us to describe the design space,
to distill the similarities between the two languages, and to
use
one proof of soundness for both. We
also prove that all execution strategies
are equivalent in the sense that all terminating executions
which
do not involve a link error, give the same result.
},
PAGES = {38--53},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/DroLagEis-ESOP03.pdf},
DARTREPORT = {yes}
}
@UNPUBLISHED{Dro+Lag+Eis-2005,
AUTHOR = {S.~Drossopoulou and G.~Lagorio and S.~Eisenbach},
TITLE = {Flexible Models for Dynamic Linking},
YEAR = {2005},
NOTE = {Submitted for journal publication},
ABSTRACT = {
Dynamic linking supports flexible code deployment, allowing
partially linked code to link further code on the fly, as needed.
Thus, end-users enjoy the advantage of automatically receiving any
updates, without any need for any explicit actions on their side,
such as re-compilation, or re-linking. On the down side, two
executions of a program may link in different versions of code,
which in some cases causes subtle errors, and may mystify
end-users.
Dynamic linking in Java and C\# are similar: The same linking
phases are involved, soundness is based on similar ideas, and
executions which do not throw linking errors give the same result.
They are, however, not identical: the linking phases are combined
differently, and take place in different order. Consequently,
linking errors may be detected at different times by Java and
C\# runtime systems.
We develop a non-deterministic model, which
describes the behaviour of both Java and C\#
program executions. The non-determinism allows us to
describe the design space, to distill the similarities between the
two languages, and to use one proof of soundness for both. We
also prove that all execution strategies are
equivalent with respect to
terminating executions that do not throw link errors: they give the same
results.
},
PDF = {http://www.disi.unige.it/person/LagorioG/dart/papers/DroLagEis-Submitted.pdf},
DARTREPORT = {yes}
}
@ARTICLE{Damiani:MSCS-03,
DARTREPORT = {yes},
ITRSPAPER = {yes},
AUTHOR = {Ferruccio Damiani},
TITLE = {A conjunctive type system for useless-code elimination},
JOURNAL = {Math.\ Structures Comput.\ Sci.},
YEAR = {2003},
VOLUME = {13},
NUMBER = {},
PAGES = {157--197},
XPUBLISHER = {Cambridge University Press}
}
@MISC{Anc+And+Dam+Dro+Gia+Zuc:2003,
AUTHOR = {Davide Ancona and Christopher Anderson and Ferruccio
Damiani and Sophia Drossopoulou and Paola Giannini
and Elena Zucca},
NOTE = {Submitted for journal publication},
TITLE = {A {\em provenly correct} translation of
{Fickle} into {Java}},
ABSTRACT = {We present a translation from ${\cal F}ickle$, a small
object-oriented language
allowing objects to
change their class at run-time, into Java.
The translation is provenly correct, in the sense that we
have shown it to preserve the static and dynamic semantics.
Moreover, it is compatible with separate compilation,
since the translation of a ${\cal F}ickle$ class does not depend on the
implementation of used classes.
Based on the formal system, we have developed
an implementation.
The translation turned out to be a more subtle problem
than we expected, and the proofs helped us uncover several
subtle errors. In this paper,
we discuss four different possible approaches we considered
for the design of the translation and justify our choice,
we present formally the translation and the proof
of preservation of the static and dynamic semantics,
and we discuss the prototype implementation.
The language ${\cal F}ickle$ has undergone, and is still
undergoing several phases
of development. In this paper we are discussing the
translation of ${\cal F}ickle_{II}$.},
DARTREPORT = {yes},
URL = {http://www.di.unito.it/~damiani/papers/FickleToJava03.html},
PDF = {http://www.di.unito.it/~damiani/papers/FickleToJava03.pdf}
}
@INPROCEEDINGS{Sca+Mic:LFM-2002,
AUTHOR = {Ivan Scagnetto and Marino Miculan},
TITLE = {Ambient Calculus and its Logic in the {C}alculus of
{I}nductive {C}onstructions},
BOOKTITLE = {Proc.~LFM~'02},
YEAR = 2002,
EDITOR = {Frank Pfenning},
NOTE = {The LFM~'02 proceedings appears as \emph{ENTCS} 70(2)},
PUBLISHER = {Elsevier},
DARTREPORT = {yes},
ABSTRACT = { The Ambient Calculus has been recently proposed
as a model of
mobility of agents in a dynamically changing hierarchy of
domains.
In this paper, we describe the implementation of the theory and
metatheory of Ambient Calculus and its modal logic in the
Calculus
of Inductive Constructions. We take full advantage of
Higher-Order
Abstract Syntax, using the Theory of Contexts as a
fundamental tool for developing formally the metatheory of the
object system. Among others, we have successfully proved a
set of
fresh renamings properties, and formalized the connection
between the Theory of Contexts and Gabbay-Pitts' "new"
quantifier.
As a feedback, we introduce a new definition of satisfaction
for the
Ambients logic and derive some of the properties originally
assumed
as axioms in the Theory of Contexts.},
PDF = {http://www.dimi.uniud.it/~miculan/Papers/LFM02.pdf}
}
@TECHREPORT{Hon+Sca:03,
AUTHOR = {Honsell, Furio and Scagnetto, Ivan},
TITLE = {Mobility types in {C}oq},
MONTH = JUN,
YEAR = 2003,
INSTITUTION = {Dipartimento di Matematica e Informatica, Universit\`a
di Udine, Italy},
DARTREPORT = {yes},
ABSTRACT = {The need for formal methods for certifying the good behaviour
of computer software is dramatically increasing with the growing
complexity of the latter. Moreover, in the global computing
framework one must face the additional issues of concurrency and
mobility. In the recent years many new process algebras have been
introduced in order to reason formally about these problems; the
common pattern is to specify a type system which allows one to
discriminate between ``good'' and ``bad'' processes. In this paper
we focus on an incremental type system for a variation of the
Ambient Calculus called M3, i.e., Mobility types for Mobile
processes in Mobile ambients and we formally prove its soundness in
the proof assistant Coq.},
PDF = {http://www.macs.hw.ac.uk/DART/reports/D2.2/HS03.pdf}
}
@INPROCEEDINGS{Cia+Liq+Mic:lpar03,
AUTHOR = {Alberto Ciaffaglione and Luigi Liquori and Marino Miculan},
TITLE = {Imperative Object-based Calculi in (Co)Inductive Type Theories },
CROSSREF = {LPAR2003},
DARTREPORT = {yes},
ABSTRACT = {We discuss the formalization of Abadi and Cardelli's
imp$\varsigma$, a
paradigmatic object-based calculus with types and side effects, in
Co-Inductive Type Theories, such as the Calculus of (Co)Inductive
Constructions (CC(Co)Ind). Instead of representing directly the
original system "as it is", we reformulate its syntax and semantics
bearing in mind the proof-theoretical features provided by the target
metalanguage. On one hand, this methodology allows for a smoother
implementation and treatment of the calculus in the metalanguage. On
the other, it is possible to see the calculus from a new perspective,
thus having the occasion to suggest original and cleaner
presentations. We give hence a new presentation of imp$\varsigma$,
exploiting natural deduction semantics, (weak) higher-order abstract
syntax, and, for a significant fragment of the calculus, coinductive
typing systems. This presentation is easier to use and implement than
the original one, and the proofs of key metaproperties, e.g. subject
reduction, are much simpler. Although all proof developments have
been carried out in the Coq system, the solutions we have devised in
the encoding of and metareasoning on imp$\varsigma$ can be applied to
other imperative calculi and proof environments with similar
features.},
PDF = {http://www.dimi.uniud.it/~miculan/Papers/LPAR03.pdf}
}
@INPROCEEDINGS{Cia+Liq+Mic:merlin03,
AUTHOR = {Alberto Ciaffaglione and Luigi Liquori and Marino Miculan},
TITLE = {Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax},
ADDRESS = {Uppsala, Sweden},
BOOKTITLE = {Proc.~2nd~MER$\lambda$IN},
YEAR = 2003,
SERIES = {ACM Digital Library},
DARTREPORT = {yes},
ORGANIZATION = {ACM},
ABSTRACT = {We illustrate the benefits of using \emph{Natural Deduction} in
combination with \emph{weak Higher-Order Abstract Syntax} for
formalizing an object-based calculus with objects, cloning,
method-update, types with subtyping, and side-effects, in inductive
type theories such as the \emph{Calculus of Inductive
Constructions}. This setting suggests a clean and compact
formalization of the syntax and semantics of the calculus, with an
efficient management of method closures. Using our
formalization and the \emph{Theory of Contexts}, we can
prove formally the Subject Reduction Theorem in the proof assistant
Coq, with a relatively small overhead.},
PDF = {http://www.dimi.uniud.it/~miculan/Papers/MERLIN03.pdf}
}
@TECHREPORT{Hon+Len:coalg-02,
AUTHOR = {F. Honsell and M. Lenisa and R. Redamalla},
TITLE = {Coalgebraic Semantics and Observational Equivalences of an Imperative Class-based OO Language},
INSTITUTION = {Dipartimento di Matematica e Informatica, Universit\`a
di Udine, Italy},
YEAR = {2003},
NUMBER = {02/2003},
DARTREPORT = {yes},
ABSTRACT = {
We study two \emph{observational equivalences} of \emph{Fickle}
programs. Fickle is a class-based object oriented imperative language,
which extends Java with object \emph{re-classification}. The first is
a \emph{contextual} equivalence of expressions with respect to a given
program. We provide an \emph{adequate} \emph{coalgebraic semantics}
for it,
which is \emph{compositional} w.r.t. the operators of the language.
The second observational equivalence is defined on programs
implementing the same specification, given as an \emph{abstract
class}. We introduce a coalgebraic description of classes which gives a sound
\emph{coinduction principle} for this latter equivalence.
To this end we need to extend the original coalgebraic approach
of H.Reichel and B.Jacobs to deal with \emph{binary
methods}, i.e. methods which take more than one instance of the
hosting class as argument. This coalgebraic description induces in
particular a
\emph{coinductive observational
equivalence} on
\emph{objects} of a program, where objects (states of a class)
are taken to be equal when the action of methods on them yield the
same \emph{observations} and equivalent next states.
},
PDF = {http://www.dimi.uniud.it/~lenisa/Papers/Soft-copy-pdf/obj.pdf}
}
@INPROCEEDINGS{Hon+Len+Red:COMETA-2003,
AUTHOR = {Furio Honsell and Marina Lenisa and Rekha Redamalla},
TITLE = {Coalgebraic Semantics and Observational Equivalences
of an Imperative Class-based OO-Language},
DARTREPORT = {yes},
BOOKTITLE = {Proc.~COMETA'03},
CROSSREF = {COMETA2003},
PAGES = {146--162},
PDF = {http://www.dimi.uniud.it/~lenisa/Papers/Soft-copy-pdf/cometa03b.pdf},
ABSTRACT = {Fickle is a class-based object oriented imperative
language, which extends Java with object
\emph{re-classification}. In this paper, we
introduce a natural \emph{observational equivalence}
over \emph{Fickle} programs. This is a
\emph{contextual} equivalence over \emph{main}
methods with respect to a given sequence of class
definitions, {i.e. a program}. In order to study it,
we utilize the formal computational model for
OO-programming based on \emph{coalgebras}, which has
recently emerged, whereby objects are taken to be
equal when the actions of methods on them yield the
same \emph{observations} and equivalent next
states. However, in order to deal with {\em
imperative features}, we need to extend the original
approach of H.Reichel and B.Jacobs in various
ways. In particular, we introduce a
\emph{coalgebraic} description of objects (states of
a class), which induces a \emph{coinductive
behavioural equivalence} on programs. For
simplicity, we focus on Fickle \emph{objects} whose
methods do not take more than one object parameter
as argument. Completeness results as well as
problematic issues arising from \emph{binary
methods} are also discussed.}
}
@ARTICLE{Pao+Ron:IC-04,
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/~ronchi/papers/cr.ps},
YEAR = 2004,
DARTREPORT = {yes}
}
@BOOK{Pao+Ron:ParLambdaCalc-03,
AUTHOR = {Ronchi Della Rocca, Simona and Paolini, Luca},
TITLE = {The Parametric Lambda-Calculus: a Metamodel for
Computation},
PUBLISHER = {Springer-Verlag},
SERIES = {Texts in Theoretical Computer Science:
An EATCS Series},
PAGES = 252,
ADDRESS = {Berlin},
YEAR = 2004,
PDF = {http://www.di.unito.it/~ronchi/papers/rpbook.pdf},
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. },
DARTREPORT = {yes}
}
@ARTICLE{Pao+Ron:ENTCS-04,
AUTHOR = {Paolini L., Ronchi Della Rocca S.},
TITLE = {Lazy Logical Semantics},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
VOLUME = {104},
PAGES = {235--251},
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.},
URL = {http://www.di.unito.it/~ronchi/papers/lazy.pdf},
YEAR = 2004,
DARTREPORT = {yes}
}
@UNPUBLISHED{Pim+Ron+Rov:SD-05,
AUTHOR = {Pimentel, Elaine and Ronchi Della Rocca, Simona and
Roversi, Luca},
TITLE = {Intersection Types: a Proof-Theoretical Approach},
NOTE = {To appear in Proceedings of STRUCTURES AND DEDUCTION
- ICALP Workshop Lisbon July 16-17},
YEAR = 2005,
PDF = {http://www.di.unito.it/~ronchi/papers/ISL.pdf},
DARTREPORT = {yes},
XREMARK = {*** replace by Pim+Ron+Rov:SD-2005 ***}
}
@INPROCEEDINGS{Pao+Pim+Ron:ITRS-04,
AUTHOR = {Paolini L., Pimentel E., Ronchi Della Rocca S.},
TITLE = {Lazy strong normalization},
BOOKTITLE = {Proceedings of Intersection Types and Related System. A satellite workshops of the Joint Meeting ICALP2004/LICS2004.},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
VOLUME = {to appear},
PAGES = {??},
ABSTRACT = { Among all the reduction strategies for the untyped
lambda-calculus, the so called lazy beta-evaluation is
of particular interest due to its large applicability to
functional programming languages (e.g. Haskell). This
strategy reduces only redexes not inside a lambda abstraction.
The lazy strongly beta-normalizing terms are the
lambda-terms that don't have infinite lazy beta-reduction sequences.
This paper presents a logical characterization of
lazy strongly beta-normalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between call-by-name and call-by-value lambda-calculus.
In fact, it turns out that the class of lazy strongly
beta-normalizing terms coincides with that of call-by-value potentially
valuable terms. This last class is of particular interest since it
is a key notion for characterizing solvability in the call-by-value setting.},
URL = {http://www.di.unito.it/~ronchi/papers/lsn.pdf},
YEAR = 2004,
NOTE = {Mario Coppo and Damiani Ferruccio editors.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Damiani+Dezani+Giannini:SAC-2004,
TITLE = {Re-classification and Multithreading: Fickle$_{MT}$},
AUTHOR = {Ferruccio Damiani and Mariangiola Dezani-Ciancaglini and Paola Giannini},
PUBLISHER = {ACM},
YEAR = {2004},
CROSSREF = {SAC-2004},
PAGES = {},
NOTE = {In OOPS track},
URL = {http://www.di.unito.it/~damiani/papers/fickleMT.html},
PDF = {http://www.di.unito.it/~damiani/papers/fickleMT.pdf},
ABSTRACT = {
In this paper we consider re-classification in the presence
of multi-threading. To this aim we define a multi-threaded
extension of the language
$Fickle$, that we call $Fickle_{MT}$. We
define an operational semantics and a type and effect system for
the language.
Each method signature carries the information on the
possible effects of the method execution. The type and effect system
statically checks this information. The operational semantics uses
this information in order to delay the execution of some threads
when this could cause ``messageNotUnderstood'' errors. We prove
that in the execution of a well-typed expression such delays do
not produce deadlock.
},
DARTREPORT = {yes}
}
@ARTICLE{Damiani-Dezani-Giannini:JOT-04,
AUTHOR = {F. Damiani and M. Dezani-Ciancaglini and P. Giannini},
TITLE = {On Re-classification and Multithreading},
JOURNAL = {Journal of Objectc Technology (www.jot.fm)},
VOLUME = {3},
NUMBER = {11},
PAGES = {5-30},
MONTH = {December},
YEAR = {2004},
NOTE = {Special issue: OOPS track at SAC 2004, Nicosia/Cyprus},
DARTREPORT = {yes},
ABSTRACT = {In this paper we consider re-classification in the presence of multi-threading. To this aim we define a multi-threaded extension of the language Fickle, that we call FickleMT. We define an operational semantics and a type and effect system for the language. Each method signature carries the information on the possible effects of the method execution. The type and effect system statically checks this information. The operational semantics uses this information in order to delay the execution of some threads when this could cause access to non-existing members of objects. We show that in the execution of a well-typed expression such delays do not produce deadlock. Lastly we discuss a translation from FickleMT into Java, showing how the operational semantics can be implemented with the standard Java multi-threading constructs.},
DOCUMENTURL = { http://www.jot.fm/issues/issue_2004_12},
PDF = {http://www.jot.fm/issues/issue_2004_12/article1/article1.pdf}
}
@INPROCEEDINGS{Wells:ICALP-2002,
ITRSPAPER = {yes},
AUTHOR = {J. B. Wells},
TITLE = {The Essence of Principal Typings},
CROSSREF = {ICALP2002},
DOCUMENTURL = {http://www.church-project.org/reports/Wells:ICALP-2002.html},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:ICALP-2002.pdf},
DARTREPORT = {yes},
CHURCHREPORT = {yes},
PAGES = {913--925},
SPRINGERURL = {http://link.springer.de/link/service/series/0558/bibs/2380/23800913.htm},
ABSTRACT = {Let $S$ be some type system. A \emph{typing} in $S$
for a typable term $M$ is the collection of all of
the information other than $M$ which appears in the
final judgement of a proof derivation showing that
$M$ is typable. For example, suppose there is a
derivation in $S$ ending with the judgement
$A\vdash{M}\mathrel{:}{\tau}$ meaning that $M$ has
result type $\tau$ when assuming the types of free
variables are given by $A$. Then $(A,\tau)$ is a
typing for $M$.
\par
A \emph{principal typing} in $S$ for a term $M$ is a
typing for $M$ which somehow represents all other
possible typings in $S$ for $M$. It is important not
to confuse this notion with the weaker notion of
\emph{principal type} often mentioned in connection
with the Hindley/Milner type system. Previous
definitions of principal typings for specific type
systems have involved various syntactic operations
on typings such as \emph{substitution} of types for
type variables, \emph{expansion}, \emph{lifting},
etc.
\par
This paper presents a new general definition of
principal typings which does not depend on the
details of any particular type system. This paper
shows that the new general definition correctly
generalizes previous system-dependent definitions.
This paper explains why the new definition is the
right one. Furthermore, the new definition is used
to prove that certain polymorphic type systems using
$\forall$-quantifiers, namely System F and the
Hindley/Milner system, do not have principal
typings.}
}
@UNPUBLISHED{Wells:EPT-2002,
ITRSPAPER = {yes},
AUTHOR = {J. B. Wells},
TITLE = {The Essence of Principal Typings},
DOCUMENTURL = {http://www.church-project.org/reports/Wells:EPT-2002.html},
PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:slightly-longer.pdf},
DARTREPORT = {yes},
CHURCHREPORT = {yes},
YEAR = 2002,
NOTE = {A longer version of \cite{Wells:ICALP-2002} with a
3-page appendix with extra proofs, a page of extra
discussion of non-related work, and other minor
changes},
ABSTRACT = {Let $S$ be some type system. A \emph{typing} in $S$
for a typable term $M$ is the collection of all of
the information other than $M$ which appears in the
final judgement of a proof derivation showing that
$M$ is typable. For example, suppose there is a
derivation in $S$ ending with the judgement
$A\vdash{M}\mathrel{:}{\tau}$ meaning that $M$ has
result type $\tau$ when assuming the types of free
variables are given by $A$. Then $(A,\tau)$ is a
typing for $M$.
\par
A \emph{principal typing} in $S$ for a term $M$ is a
typing for $M$ which somehow represents all other
possible typings in $S$ for $M$. It is important not
to confuse this notion with the weaker notion of
\emph{principal type} often mentioned in connection
with the Hindley/Milner type system. Previous
definitions of principal typings for specific type
systems have involved various syntactic operations
on typings such as \emph{substitution} of types for
type variables, \emph{expansion}, \emph{lifting},
etc.
\par
This paper presents a new general definition of
principal typings which does not depend on the
details of any particular type system. This paper
shows that the new general definition correctly
generalizes previous system-dependent definitions.
This paper explains why the new definition is the
right one. Furthermore, the new definition is used
to prove that certain polymorphic type systems using
$\forall$-quantifiers, namely System F and the
Hindley/Milner system, do not have principal
typings.}
}
@COMMENT{{PeterhasdroppedthenextentryasaChurchreportinfavorofWells:APAL-1999-v98-no-notebelow.Thishasbeendoneafter2unrespondede-mailstotheauthor.PleasecontactPeterbeforeturningitintoaChurchReport.}}
@ARTICLE{Dez+Hon+Ale:TOCL-2003,
ITRSPAPER = {yes},
AUTHOR = {M. {Dezani-Ciancaglini} and F. Honsell and F. Alessi},
TITLE = {A Complete Characterization of Complete Intersection-Type Preorders},
JOURNAL = {{ACM} Transactions on Logic and Computation},
VOLUME = {4},
NUMBER = {1},
PAGES = {120--147},
MONTH = JAN,
YEAR = {2003},
PDF = {http://www.di.unito.it/~dezani/papers/tocl03.pdf},
ABSTRACT = {We characterize those ``type preorders'' which yield
complete ``intersection-type assignment systems'' for
lambda calculi, with respect to the three canonical 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 the ``intersection constructor,
set-theoretic intersection, and by taking the interpretation
of the ``arrow constructor'', a la Scott, with
respect to either ``any possible functionality set'', or the ``largest'' one, or
the ``least'' one.
These results strengthen and generalize significantly all earlier
results in the literature, to our 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 of
restricted lambda calculi. Nevertheless the characterizations we give
can
be tailored just to the case of lambda models.
},
DARTREPORT = {yes}
}
@ARTICLE{Dro+Dez+Dam+Gia:TOPLAS-2002,
AUTHOR = {S. Drossopoulou and F. Damiani and M.
{Dezani-Ciancaglini}
and P. Giannini},
TITLE = {More Dynamic Object Re-classification: Fickle{II}},
JOURNAL = {{ACM} Trans.\ on Prog.\ Langs.\ {\&} Systs.},
VOLUME = {24},
NUMBER = {2},
PAGES = {153--191},
MONTH = MAR,
YEAR = {2002},
DISABLEDDOCUMENTURL = {http://www.di.unito.it/~damiani/papers/dor.html},
PDF = {http://www.di.unito.it/~damiani/papers/dor.pdf},
ABSTRACT = {Re-classification changes at run-time the class
membership of
an object while retaining its identity. We suggest language
features for
object re-classification, which could extend an imperative,
typed,
class-based, object-oriented language. We present our proposal
through the
language Fickle (Fickle is the successor of an earlier
proposal, Fickle-99;
although both Fickle and Fickle-99 address the same
requirement for object
re-classification, the approaches are very different). The
imperative
features combined with the requirement for a static and safe
type system
provided the main challenges. We develop a type and effect
system for Fickle
and prove its soundness with respect to the operational
semantics.
In particular, even though objects may be re-classified across
classes with
different members, they will never attempt to access
non-existing members.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Dam+Dez+Dro+Gia:2002,
AUTHOR = {F. Damiani and M.
{Dezani-Ciancaglini} and S. Drossopoulou
and P. Giannini},
TITLE = {Refined Effects for Re-classification: Fickle{III}},
MONTH = DEC,
NOTE = {Internal report},
YEAR = {2002},
PDF = {http://www.di.unito.it/~damiani/papers/rer.pdf},
ABSTRACT = {Re-classification changes at run-time the class
membership of
an object while retaining its identity.
In our previous work on the language
FickleII~\cite{Dro+Dam+Dez+Gia:TOPLAS-2002}
we suggest language
features for
object re-classification, which could extend an imperative,
typed,
class-based, object-oriented language.
In this paper we present the language FickleIII, which improves
FickleII with a more expressive type and effect system.
FickleIII allows to correctly type
meaningful programs which FickleII reject. This is done by
taking into account the
initial and the final class of each re-classification.
The syntax
of FickleIII and the syntax of FickleII differ only in the effect
annotations occurring in methods' signatures (every FickleII-style
effect annotation can be coded into a FickleIII-style effect
annotation, but not vice versa). The operational semantics (which
ignores effect annotations) is unchanged.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Ale+Bar+Dez:WOLLIC-2003,
ITRSPAPER = {yes},
AUTHOR = {F. Alessi and F. Barbanera and M. {Dezani-Ciancaglini}},
TITLE = {Intersection Types and Computational Rules},
BOOKTITLE = {WoLLIC '03},
YEAR = {2003},
SERIES = {ENTCS},
VOLUME = {82},
MONTH = {August},
PUBLISHER = {Elsevier},
PDF = {http://www.di.unito.it/~dezani/papers/wollic03.pdf},
ABSTRACT = {
The invariance of the meaning
of a lambda term by reduction/expansion w.r.t. the considered computational rules
is one of the minimal requirements one expects to hold 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
type 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.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{And+Bar+Dez+Dros:WOOD-2003,
AUTHOR = {C. Anderson and F. Barbanera and M.
{Dezani-Ciancaglini} and S. Drossopoulou},
TITLE = {Can Addresses be Types?
(a case study: objects with delegation)},
BOOKTITLE = {WOOD '03},
YEAR = {2003},
SERIES = {ENTCS},
VOLUME = {82},
PAGES = {},
PUBLISHER = {Elsevier},
PDF = {http://www.di.unito.it/~dezani/papers/wood03.pdf},
ABSTRACT = {
We adapt the ``aliasing constraints'' approach for designing a flexible
typing of evolving objects. Types
are singleton types (addresses of objects, as a matter of fact) whose
relevance is mainly due to the sort
of ``safety property'' they guarantee.
In particular we provide a type system for an imperative object based
calculus
with delegation and which supports method and delegate overriding,
addition, and removing.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{And+Gia:JST-2004,
AUTHOR = {Christopher Anderson and Paola Giannini},
TITLE = {Type Checking for {JavaScript}},
BOOKTITLE = {WOOD'04},
YEAR = 2004,
ABSTRACT = {JavaScript is a powerful imperative object based
language made popular by its use in web pages. It
supports flexible program development by allowing
dynamic addition of members to objects. Code is
dynamically typed: a runtime access to a
non-existing member causes an error.
\par
We suggest a static type system for JavaScript that
will detect such runtime type errors. Therefore,
programmers can have the benefit of flexible
programming offered by JavaScript with the safety
offered by a static type system.
\par
We demonstrate our type system with a formalism of
JavaScript, JS0. Our type system is based on
structural recursive types. Members of a type are
classified into definite and potential. The type of
an object can evolve through assignment to potential
members which turns them to definite. We first
present the type system with integer and object
types, and then add type variables to have
polymorphism \`{a} la ML. We prove that our type
system is sound.},
DARTREPORT = {yes},
PDF = {http://www.binarylord.com/work/js0wood.pdf}
}
@INPROCEEDINGS{And+Gia+Dro:JST-2004,
AUTHOR = {Christopher Anderson and Paola Giannini and Sophia Drossopoulou},
TITLE = {Type Inference for Scripting Languages},
CROSSREF = {ECOOP2005},
ABSTRACT = {JavaScript is a powerful imperative object based language made popular by
its use in web pages. It supports flexible program development by
allowing dynamic addition of members to objects. Code is dynamically
typed: a runtime access to a non-existing member causes an error.
\par
In this paper we first develop a formalism of JavaScript, JS0, and a static type system
that will detect such type errors. Thus, programmers can benefit from
the flexible programming style offered by JavaScript
and from the safety offered by a static type system. Our types are structural and allow objects to
evolve in a controlled manner by classifying members as definite or
potential. A potential member becomes definite upon assignment. We
prove soundness of our type system.
We then define a type inference algorithm for JS0 that is sound with
respect to the type system. If the type inference algorithm succeeds, then
the program is typeable. Therefore, programmers can benefit from the safety offered by
the type system, without the need to write explicitly types in
their programs. },
DARTREPORT = {yes},
PDF = {http://binarylord.com/work/js0/js0.pdf}
}
@INPROCEEDINGS{Smi+Dro:Traits-2004,
AUTHOR = {Charles Smith and Sophia Drossopoulou},
TITLE = {Typed Traits for Java},
CROSSREF = {ECOOP2005},
ABSTRACT = {Traits support the factoring out
of common behaviour, and its integration
into classes in a manner which smoothly coexists with inheritance-based
structuring mechanisms.
We designed the language Chai, which incorporates
statically typed traits into Java, and we discuss three versions
of the language: Chai$^1$, where traits are only a mechanism
for the creation of classes; Chai$^2$, where traits are a mechanism
for the creation of classes, {\em and} can also introduce
types, and
Chai$^3$, where traits play a role at runtime, and can
can be applied to objects, and change the objects' behaviour.
We give formal models for these languages, outline the
proof of soundness, and our prototype implementation.},
DARTREPORT = {yes},
PDF = {http://slurp.doc.ic.ac.uk/pubs/chaitraits-ecoop05.pdf}
}
@ARTICLE{And+Bar+Dez:2003,
AUTHOR = {Christopher Anderson and Franco Barbanera and Mariangiola Dezani-Ciancaglini},
TITLE = {Alias and {U}nion Types for {D}elegation},
JOURNAL = {Ann.\ Math., Comput.\ \& Teleinformatics},
VOLUME = {1},
PAGES = {1--18},
YEAR = {2003},
PDF = {http://binarylord.com/work/deltaunion.pdf},
ABSTRACT = {
We adapt the aliasing constraints approach
for designing a flexible typing of evolving objects. Types
are singleton types (addresses of objects, as a matter
of fact) or finite unions of these. Their relevance is
mainly due to the sort of safety property they guarantee.
In particular we provide a type system for an imperative
object based calculus with delegation and conditional
expressions and which supports method and delegate
overriding, addition, and removing.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Ven:Coordination-2004,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {O'{K}laim: a coordination language with mobile mixins},
BOOKTITLE = {Proceedings of COORDINATION 2004},
VOLUME = {2949},
PAGES = {20-37},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
YEAR = {2004},
PDF = {http://www.di.unito.it/~bono/papers/oklaim.pdf},
ABSTRACT = {This paper presents O'Klaim{} (Object-Oriented Klaim),
a linguistic
extension of the higher-order calculus for mobile processes Klaim
with object-oriented features. Processes interact by an
asynchronous communication model: they can distribute and retrieve
resources, sometimes structured as incomplete classes, i.e., mixins,
to and from distributed tuple spaces. This mechanism is coordinated
by providing a subtyping relation on classes and mixins, which
become polymorphic items during communication. We propose a static
typing system for: (i) checking locally each process in its own
locality; (ii) decorating object-oriented code that is sent to
remote sites with its type. This way, tuples can be dynamically
retrieved only if they match by subtyping with the expected type.
If this pattern matching succeeds, the so retrieved code can be
composed with local code, dynamically and automatically, in a
type-safe way. Thus a global safety condition is guaranteed without
requiring any additional information on the local reconfiguration of
local and foreign code, and, in particular, without any further type
checking. Finally, we present main issues concerning the
implementation of O'Klaim.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Bet+Bon+Ven:momisubtype,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {Mixin and Class Subtyping Hierarchies in a Mobile Setting},
MONTH = DEC,
YEAR = {2003},
PDF = {http://www.di.unito.it/~bono/papers/momisubtype.pdf},
ABSTRACT = {In sequential class- and mixin-based settings, subtyping is
essentially a run-time relation on objects. Either no subtyping
relation is defined on classes and mixins, or, as in Java-like
languages, classes are not ``first-class citizens'', in the sense
they cannot be passed as arguments to methods, be returned as
results to method calls, or combined in order to get new data
structures. A motivation for considering classes (and mixins) as
``first-class citizens'' that come equipped with a subtyping
relation arises from the mobile and distributed process realm, where
object-oriented code might be exchanged among the sites of a
network. In such a setting, subtyping on classes and mixins is a
tool to allow a flexible yet safe communication, because a piece of
code will be accepted on a site only if its type is
``subtyping-compliant'' with the expected type required by the
receiver. However, exposing mixin and class hierarchies to subtyping
brings in conflicts similar to the ones present in the object-based
setting: (i) component addition versus subtyping-in-width;
(ii) component override versus subtyping-in-depth. In this
paper we show formally how to solve both conflicts.},
NOTE = {Manuscript},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:FOOL-2004,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Mixin-Based Incomplete Objects},
YEAR = {2004},
BOOKTITLE = {Proceedings of FOOL 11},
PDF = {http://www.di.unito.it/~bono/papers/inc-obj.pdf},
ABSTRACT = {We design a calculus that combines class-based
features with object-based ones, with the aim of fitting into a
unifying setting the ``best of both worlds''. In a mixin-based approach,
mixins are seen incomplete classes from which
incomplete objects can be instantiated. In turn, incomplete
objects can be completed in an object-based fashion. Our hybrid
calculus is shown to be useful in some real world scenarios that
we present as examples.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:inc-obj-sub,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {Safe object composition in the presence of subtyping},
BOOKTITLE = {Proceedings of ICTCS 2005},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
YEAR = {2005},
PDF = {http://www.di.unito.it/~bono/papers/ictcs05.pdf},
ABSTRACT = {Object composition arises as a natural operation to combine objects
in an object-based setting. In our incomplete objects setting, it
has a strong meaning, as it may combine objects with different
internal states. In this paper, we study how to make object
composition safe in the presence of width subtyping: we propose
two solutions, and discuss alternative ones.},
NOTE = {To appear},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:mixin-high,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Higher-Order Mixins and Classes},
BOOKTITLE = {Post-Proceedings of Types 2003},
VOLUME = {3085},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
YEAR = {2004},
PDF = {http://www.di.unito.it/~bono/papers/mixin-high.pdf},
ABSTRACT = {This work presents an object-oriented calculus based on
higher-order mixin construction via mixin composition,
where some software engineering requirements are modeled in a formal
setting allowing to prove the absence of
message-not-understood run-time errors. Mixin composition is
shown to be a valuable language feature enabling a cleaner
object-oriented design and development. In what we believe being
quite a general framework, we give directions for designing a
programming language equipped with higher-order mixins, although our
study is not based on any already existing object-oriented language.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:SAC-2004,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Higher-Order Mixins and Classes
[Poster Abstract]},
CROSSREF = {SAC-2004},
PUBLISHER = {ACM Press},
YEAR = {2004},
PDF = {http://www.di.unito.it/~bono/papers/mixin-high-poster.pdf},
ABSTRACT = {This work presents an object-oriented calculus based on
higher-order mixin construction via mixin composition,
where some software engineering requirements are modeled in a formal
setting allowing to prove the absence of
message-not-understood run-time errors. Mixin composition is
shown to be a valuable language feature enabling a cleaner
object-oriented design and development. In what we believe being
quite a general framework, we give directions for designing a
programming language equipped with higher-order mixins, although our
study is not based on any already existing object-oriented language.},
NOTE = {In PL track. Accepted as a 2-page Poster Abstract.
Extended abstract of \cite{Bet+Bon+Lik:mixin-high}},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:SAC-2005,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {Safe and {F}lexible {O}bjects},
BOOKTITLE = {ACM Symposium on Applied Computing (SAC 2005)},
NOTE = {In OOPS track},
PUBLISHER = {ACM Press},
YEAR = {2005},
PDF = {http://www.di.unito.it/~bono/papers/SAC2005.pdf},
ABSTRACT = {We design a calculus where objects are created by instantiating
classes, as well as mixins. Mixin-instantiated objects are ``incomplete
objects'', that can be completed in object-based fashion. The
combination of class-based features with object-based ones offers
some flexible programming solutions. The fact that all objects are
created from fully-typed constructs is a guarantee of controlled
(therefore reasonably safe) behavior.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Lik:OOPSLA-2004,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Mixins and Incomplete Objects},
BOOKTITLE = {The OOPSLA Companion},
PUBLISHER = {ACM Press},
YEAR = {2004},
PDF = {http://www.di.unito.it/~bono/papers/oopsla04poster.pdf},
ABSTRACT = {Our calculus combines class-based features with object-based ones,
with the aim of fitting into a unified setting the ``best of both
worlds''. In a mixin-based approach, mixins are seen as incomplete
classes from which incomplete objects can be instantiated.
Incomplete objects can be completed in an object-based fashion.},
NOTE = {Accepted as a 2-page Poster Abstract},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bon+Tiu+Urz:typeinf,
AUTHOR = {V. Bono and J. Tiuryn and Pawel Urzyczyn},
TITLE = {Type Inference for Nested Self Types (Extended
Abstract)},
PDF = {http://www.di.unito.it/~bono/papers/typeinf.pdf},
BOOKTITLE = {Post-Proceedings of Types 2003},
VOLUME = {3085},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
YEAR = {2004},
ABSTRACT = {We address the issue of decidability of the type
inference problem for a type system of an object-oriented
calculus with general selftypes.
The fragment considered in the present paper is obtained by
restricting the set of operators to the method invocation
only. The resulting system, despite its syntactical
simplicity, is sufficiently complicated to merit
the study of the intricate constraints emerging in the
process of type reconstruction, and it can be considered as the core
system with respect to typability for extensions with other operators.
The main result of the paper is the
decidability of type reconstruction,
together with a certain form of a principal type property.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{klaim2003,
AUTHOR = {L. Bettini and V. Bono and R. De Nicola and G. Ferrari and
D. Gorla and M. Loreti and E. Moggi and R. Pugliese
and E. Tuosto and B. Venneri},
TITLE = {The {K}laim {P}roject: Theory and Practice},
BOOKTITLE = {Global {C}omputing - {P}rogramming {E}nvironments, {L}anguages,
{S}ecurity and {A}nalysis of {S}ystems},
PUBLISHER = {Springer-Verlag},
YEAR = {2003},
SERIES = {LNCS},
VOLUME = {2874},
PDF = {http://www.di.unito.it/~bono/papers/klaim-gen.pdf},
ABSTRACT = {Klaim (Kernel Language for Agents Interaction and
Mobility) is an experimental language specifically designed to
program distributed systems consisting of several mobile
components that interact through multiple distributed tuple
spaces. Klaim primitives allow programmers to distribute and
retrieve data and processes to and from the nodes of a net.
Moreover, localities are first-class citizens that can be
dynamically created and communicated over the network. Components,
both stationary and mobile, can explicitly refer and control the
spatial structures of the network.
This paper reports the experiences in the design and development
of Klaim. Its main purpose is to outline the theoretical
foundations of the main features of Klaim and its programming
model. We also present a modal logic that permits reasoning about
behavioural properties of systems and various type systems that
help in controlling agents movements and actions. Extensions of
the language in the direction of object oriented programming are
also discussed together with the description of the implementation
efforts which have lead to the current prototypes.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bono:tutorial,
AUTHOR = {V. Bono},
TITLE = {Extensible Objects: a Tutorial},
BOOKTITLE = {Global {C}omputing - {P}rogramming {E}nvironments, {L}anguages,
{S}ecurity and {A}nalysis of {S}ystems},
PUBLISHER = {Springer-Verlag},
YEAR = {2003},
SERIES = {LNCS},
VOLUME = {2874},
PDF = {http://www.di.unito.it/~bono/papers/tut.pdf},
ABSTRACT = {In the object-oriented realm, class-based languages
dominate the world of production languages, but object-based
languages have been extensively studied to provide the foundations
of the object-oriented paradigm. Moreover, object-based languages
are undergoing a Renaissance thanks to the growing popularity of
scripting languages, which are essentially object-based.
We focus on extensible object-based calculi, which feature
method addition, together with classical method override and
method invocation. Extensible objects can be seen as a way to
bridge the gap between the class-based setting and the pure
object-based setting.
Our aim is to provide a brief but rigorous view on extensible
objects, following a thread suggested by the concept of ``self''
(which is the reference to the executing object) and its related
typing problems.
This tutorial may be seen as a complementary contribution to the
literature which has explored and compared extensively pure
object-based and class-based foundations (for example, as in the
books by Abadi and Cardelli, and Bruce, respectively), but which
generally neglected extensible objects.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bon+Dam+Gia:F-WAN-2002,
AUTHOR = {V. Bono and F. Damiani and P. Giannini},
TITLE = {A calculus for ``environment-aware'' computation},
BOOKTITLE = {F-WAN '02},
YEAR = {2002},
SERIES = {ENTCS},
VOLUME = {66.3},
PAGES = {},
PUBLISHER = {Elsevier},
PDF = {http://www.di.unito.it/~damiani/papers/fwan02.pdf},
ABSTRACT = {We present a calculus for modelling
``environment-aware''
computations, that is computations that adapt their behaviour
according
to the capabilities of the environment. The calculus is an
imperative,
object-based language with extensible objects, equipped with
a labelled
transition semantics. A notion of bisimulation, lifting to
computations
a correspondence between the capabilities of different
environments,
is provided. Bisimulation can be used to prove that a program
is
``cross-environment'', i.e., it has the same behaviour when
run in
different environments.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Dam+Gia:WOOD-2003,
AUTHOR = {F. Damiani and P. Giannini},
TITLE = {Alias types for ``environment-aware'' computations},
BOOKTITLE = {WOOD '03},
YEAR = {2003},
SERIES = {ENTCS},
VOLUME = {82},
PAGES = {},
PUBLISHER = {Elsevier},
PS = {http://www.di.unito.it/~damiani/papers/wood03.ps},
URL = {http://www.di.unito.it/~damiani/papers/wood03.html},
PDF = {http://www.di.unito.it/~damiani/papers/wood03.pdf},
ABSTRACT = {
In previous work we introduced a calculus for modelling ``environment-aware''
computations, that is computations that adapt their behavior
according to the capabilities of the environment. The calculus is
an imperative, object-based language (with extensible objects
and primitives for discriminating the presence or absence of attributes of
objects) equipped with a small-step operational semantics.
In this paper we define a type and effect system for the calculus.
The typing judgements specify, via constraints,
the shape of environments which guarantees the correct execution of
expressions and the typing rules track the effect of expression evaluation
on the environment.
The type and effect system is sound w.r.t. the operational
semantics of the language.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Cop+Dez:VMCAI-2002,
ITRSPAPER = {yes},
TITLE = {A Fully Abstract Model for Higher-Order Mobile
Ambients},
AUTHOR = {M. Coppo and M. {Dezani-Ciancaglini}},
BOOKTITLE = {VMCAI 2002},
YEAR = {2002},
SERIES = {LNCS},
VOLUME = {2294},
PAGES = {255--271},
PDF = {http://www.di.unito.it/~dezani/papers/vmcai02.pdf},
ABSTRACT = {Aim of this paper is to develop a filter model for
a calculus
with mobility and higher-order value passing. We will define it
for an extension of the Ambient Calculus in which processes can
be passed as values. This model turns out to be fully abstract
with respect to the notion of contextual equivalence where the
observables are ambients at top level.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Damiani:2002,
AUTHOR = {F. Damiani},
TITLE = {Rank 2 intersection types for local definitions and
conditional expressions},
MONTH = OCT,
YEAR = 2002,
NOTE = {Supersedes~\cite{Damiani:FOSSACS-2000}. Superseded
by~\cite{Damiani:TOPLAS-2003}},
PDF = {http://www.macs.hw.ac.uk/DART/reports/D2.1/Dam02.pdf},
ABSTRACT = {We introduce a rank 2 intersection type system
with new typing
rules for local definitions (LET-expressions and
LETREC-expressions) and conditional expressions
(IF-expressions and MATCH-expressions). This is a further
step towards the use of intersection types in ``real''
programming
languages.
The technique for typing local definitions relies entirely on
the
principal typing property (i.e. it does not depend on
particulars
of rank 2 typing), so it can be applied to any system with
principal typings. The technique for typing conditional
expressions, which is based on the idea of introducing metrics
on
types to ``limit the use'' of the intersection type
constructor in
the types assigned to the branches of the conditionals, is
instead
tailored to rank 2 intersection. However, the underlying idea
might be useful also for other type systems.},
DARTREPORT = {yes}
}
@ARTICLE{Damiani:TOPLAS-2003,
ITRSPAPER = {yes},
AUTHOR = {F. Damiani},
TITLE = {Rank 2 intersection types for local definitions
and conditional expressions},
JOURNAL = {{ACM} Trans.\ on Prog.\ Langs.\ {\&} Systs.},
YEAR = {2003},
VOLUME = {25},
NUMBER = {4},
PAGES = {401--451},
DISABLEDDOCUMENTURL = {http://www.di.unito.it/~damiani/papers/tr02.html},
PDF = {http://www.di.unito.it/~damiani/papers/tr02.pdf},
ABSTRACT = {We introduce a rank 2 intersection type system
with new typing
rules for local definitions (LET-expressions and
LETREC-expressions) and conditional expressions
(IF-expressions and MATCH-expressions). This is a further
step towards the use of intersection types in ``real''
programming
languages.
The technique for typing local definitions relies entirely on
the
principal typing property (i.e. it does not depend on
particulars
of rank 2 typing), so it can be applied to any system with
principal typings. The technique for typing conditional
expressions, which is based on the idea of introducing metrics
on
types to ``limit the use'' of the intersection type
constructor in
the types assigned to the branches of the conditionals, is
instead
tailored to rank 2 intersection. However, the underlying idea
might be useful also for other type systems.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Ven:Coordination-2002,
TITLE = {Coordinating Mobile Object-Oriented Code},
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
BOOKTITLE = {Coordination 2002},
YEAR = {2002},
SERIES = {LNCS},
VOLUME = {2315},
PAGES = {56--71},
PDF = {http://www.di.unito.it/~bono/papers/COORD02.pdf},
ABSTRACT = {Standard class-based inheritance mechanisms, which are often
used to implement distributed systems, do not seem to scale well to a
distributed context with mobility. In this paper, a ``mixin''-based
approach is proposed for structuring mobile object-oriented code and it
is shown to fit in the dynamic and open nature of a mobile code scenario.
We introduce MoMi (Mobile Mixins), a coordination language for mobile
processes that communicate and exchange object-oriented code in a distributed
context. MoMi is equipped with a type system, based on polymorphism by
subtyping, in order to guarantee ``safe'' code communications.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Bet+Bon+Ven:momiwidth,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {{M}o{M}i - {A} {C}alculus for {M}obile {M}ixins},
MONTH = JAN,
YEAR = {2003},
PDF = {http://www.di.unito.it/~bono/papers/momiwidth.pdf},
ABSTRACT = {MoMi (Mobile Mixins) is a coordination language for mobile
processes that communicate and exchange object-oriented code in a
distributed context. MoMi's key idea is structuring mobile
object-oriented code by using mixin-based inheritance. Mobile code
is compiled and typed locally, and can successfully interact with
code present on foreign sites only if its type is
subtyping-compliant with the type of what is expected by the receiving site.
The key feature of the paper is the definition of this subtyping relation
on classes and mixins that enables a significantly flexible, yet
still simple, communication pattern. We show that communication by
subtyping is type safe in that exchanged code is merged into local
code without requiring further type analysis and recompilation.},
NOTE = {Manuscript},
DARTREPORT = {yes}
}
@UNPUBLISHED{Bet+Bon+Ven:momiwidth-2004,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {{M}o{M}i - {A} {C}alculus for {M}obile {M}ixins},
YEAR = {2005},
PDF = {http://www.di.unito.it/~bono/papers/momiwidth-2005.pdf},
ABSTRACT = {MoMi (Mobile Mixins) is a coordination language for mobile
processes that communicate and exchange object-oriented code in a
distributed context. MoMi's key idea is structuring mobile
object-oriented code by using mixin-based inheritance. Mobile code
is compiled and typed locally, and can successfully interact with
code present on foreign sites only if its type is
subtyping-compliant with the type of what is expected by the receiving site.
The key feature of the paper is the definition of this subtyping relation
on classes and mixins that enables a significantly flexible, yet
still simple, communication pattern. We show that communication by
subtyping is type safe in that exchanged code is merged into local
code without requiring further type analysis and recompilation.},
NOTE = {This work improves \cite{Bet+Bon+Ven:momiwidth}. To appear
in Acta Informatica, Special Issue on ``Types in Concurrency'' (this
version is therefore a more complete one w.r.t. the version at month 30)},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bet+Bon+Ven:TCS-2004,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
CROSSREF = {TCS2004},
TITLE = {Subtyping-Inheritance Conflicts: The Mobile Mixin Case},
PDF = {http://www.di.unito.it/~bono/papers/tcs2004.pdf},
ABSTRACT = {In sequential class- and mixin-based settings, subtyping is
essentially a relation on objects: no subtype relation is defined on
classes and mixins, otherwise there would be conflicts with
the inheritance mechanism, creating type un-safety. Nevertheless,
a width-depth subtyping relation
on class and mixin types is useful in the realm of mobile and
distributed processes, where object-oriented code may be exchanged
among the sites of a net. In our proposal, classes and mixins
become ``first-class citizens'' at communication time, and
communication is ruled by a type-safe width-depth subtyping
relation.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{deLiguoro:ITRS-2002,
ITRSPAPER = {yes},
TITLE = {Subtyping in logical form},
AUTHOR = {U. de' Liguoro},
BOOKTITLE = {Proceedings of ITRS'02},
YEAR = {2002},
SERIES = {ENTCS},
VOLUME = {70.1},
PAGES = {16},
PDF = {http://www.di.unito.it/~deligu/pub/dL02.pdf},
ABSTRACT = {By using intersection types and filter models we
formulate a
theory of subtyping via a finitary programming logic. Types are
interpreted as spaces of filters over a subset of the language
of
properties (the intersection types) which describes the
underlying
type free realizability structure. We show that such an
interpretation coincides with a PER semantics, proving that the
quotient space arising from ``logical'' PERs taken with the
intrinsic ordering is isomorphic to the filter semantics of
types.
As a byproduct we obtain a semantic proof of soundness of the
logic semantics of terms and equation of a typed lambda calculus
with record subtyping.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Dez+Fri+Gio+Mot:ITRS-2002,
ITRSPAPER = {yes},
AUTHOR = {M. {Dezani-Ciancaglini} and A. Frisch and E.
Giovannetti and
Y. Motohama},
TITLE = {The Relevance of Semantic Subtyping},
BOOKTITLE = {ITRS 2002},
YEAR = {2002},
PUBLISHER = {Elsevier},
SERIES = {ENTCS},
VOLUME = {70.1},
PAGES = {},
ABSTRACT = {We compare Meyer and Routley's minimal relevant
logic B+ with
the recent semantics-based approach to subtyping
introduced by
Frisch, Castagna and Benzaken in the definition
of a type
system with intersection and union. We show that
-- for the
functional core of the system -- such notion of
subtyping,
which is defined in purely set-theoretical
terms, coincides
with the relevant entailment of the logic B+.},
PDF = {http://www.di.unito.it/~dezani/papers/itrs02.pdf},
DARTREPORT = {yes}
}
@TECHREPORT{Bru+Hon+Len+Mic:UD-TR-21-02,
AUTHOR = {R. Bruni and F. Honsell and M. Lenisa and
M. Miculan},
TITLE = {Modeling Fresh Names in pi-calculus Using
Abstractions},
YEAR = 2002,
DARTREPORT = {yes},
INSTITUTION = {Dipartimento di Matematica e Informatica,
Universit\`a di Udine,
Italy},
NUMBER = {TR-21-02},
ABSTRACT = {In this paper, we model fresh names in the
pi-calculus using
\emph{abstractions} w.r.t. a new binding operator $\theta$.
Both
the theory and the metatheory of the $\pi$-calculus benefit
from
this simple extension. The operational semantics of this new
calculus is \emph{finitely branching}. Bisimulation can be
given
without mentioning any constraint on names, thus allowing for a
straightforward definition of a \emph{coalgebraic} semantics.
This
is cast within a category of coalgebras over algebras with
infinitely many unary operators, in order to capitalize on
$\theta$.
Following previous work by Montanari and Pistore, we present
also a
\emph{finite} representation for \emph{finitary} processes and
a
finite state verification procedure for bisimilarity, based on
the
new notion of \emph{$\theta$-automaton}. Finally, we improve
previous encodings of the $\pi$-calculus in the Calculus of
Inductive Constructions. },
PDF = {http://www.dimi.uniud.it/~lenisa/Papers/Soft-copy-pdf/pitheta.pdf}
}
@TECHREPORT{Cia+DiG+Hon+Liq:ext-02,
AUTHOR = {A. Ciaffaglione and P. Di Gianantonio and F. Honsell
and L. Liquori},
TITLE = {Foundations for dynamic object re-classification},
INSTITUTION = {Dipartimento di Matematica e Infomatica, Universita'
di Udine, Italy},
YEAR = {2003},
NUMBER = {03/2003},
DARTREPORT = {yes},
ABSTRACT = {%
We investigate, in the context of {\em functional prototype-based
languages}, objects which might extend themselves upon
receiving a message. The possibility for an object of extending its
own ``self'', referred to by Cardelli as a {\em self-inflicted}
operation, is novel in the context of typed object-based languages. We
present a sound type system for this calculus which guarantees that
evaluating a well-typed expression will never yield a {\tt
message-not-found} run-time error. The resulting calculus appears to
be also a good starting point for a rigorous mathematical analysis of
class-based languages.
Our contribute can be viewed as a theoretical and sound foundation for
\emph{dynamic object re-classification} underpinned on
\emph{functional programming paradigm}. Re-classification changes at
run-time the class membership of an object while retaining its
identity. An imperative approach to re-classification, suggesting
language features, has been undertaken through the language
\texttt{Fickle}. },
PDF = {http://www.dimi.uniud.it/~ciaffagl/Objects/selfinflrecl.pdf}
}
@PHDTHESIS{Cia:PhD-2003,
AUTHOR = {Alberto Ciaffaglione},
TITLE = {Certified reasoning on Real Numbers and Objects in
Co-inductive Type Theory},
INSTITUTION = {{Ph.D. Thesis}},
SCHOOL = {Dipartimento di Matematica e Informatica
Universit\`a di Udine, Italy},
YEAR = 2003,
DARTREPORT = {yes},
NOTE = {available as outline},
ABSTRACT = { In the thesis we adopt Type Theory-based Formal
Methods, namely
the proof assistant Coq, for reasoning on two distinct topics.
In the first part we encode the Constructive Real Numbers in Coq using
infinite sequences of digits. Then we work on such a representation
with co-inductive types and co-recursive proofs. The final aim is to
prove in Coq that the representation satisfies a set of axioms,
proposed for characterizing the constructive reals.
In the second part we encode the Abadi-Cardelli's imp-\varsigma
calculus in Coq using an higher-order approach. We formalize the
syntax, the first-order static semantics and the big-step dynamic
semantics. Then we prove a Subject Reduction theorem relating the
two semantics. The ultimate goal is to obtain a Type Soundness
result in Coq.
},
PDF = {http://www.dimi.uniud.it/~ciaffagl/Objects/impvarsigma.pdf}
}
@INPROCEEDINGS{Dez+Lus:WIT-2002,
ITRSPAPER = {yes},
AUTHOR = {M. {Dezani-Ciancaglini} and S. Lusin},
TITLE = {Intersection Types and Lambda Theories},
BOOKTITLE = {WIT 2002},
YEAR = {2002},
ABSTRACT = {We illustrate the use of intersection types as a
semantic tool
for showing properties of the lattice of lambda
theories. Relying
on the notion of easy intersection type theory
we successfully
build a filter model in which the interpretation
of an arbitrary
simple easy term is any filter which can be
described in an
uniform way by a recursive predicate. This
allows us to prove
the consistency of a well-know lambda theory:
this consistency
has interesting consequences on the algebraic
structure of the
lattice of lambda theories.},
XSERIES = {Electronic proceedings},
URL = {http://www.irit.fr/zeno/WIT2002/proceedings.shtml},
PDF = {http://www.di.unito.it/~dezani/papers/wit02.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Cop+Dez+Gio-Sal:CATS-2003,
AUTHOR = {M. Coppo and M. {Dezani-Ciancaglini} and
E. Giovannetti and I. Salvo},
TITLE = {M3: Mobility Types for Mobile Processes in Mobile
Ambients},
BOOKTITLE = {CATS 2003},
YEAR = {2003},
ABSTRACT = {We present an ambient-like calculus in which the
open
capability is
dropped, and
a new form of ``lightweight" process mobility is
introduced.
The calculus comes equipped with a
type system which allows
the kind of values exchanged in communications
and the access and
mobility properties of processes to be controlled.
A type inference procedure determines
the ``minimal" requirements to accept a system or
a component
as well
typed.
This gives a kind of principal type.
As an expressiviness test, we show that some of
the most known
calculi of
concurrency and mobility can be encoded in our
calculus in a
natural way.},
SERIES = {ENTCS},
VOLUME = {78},
PDF = {http://www.di.unito.it/~dezani/papers/cats03.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{vBak+Dez:LATIN-2002,
ITRSPAPER = {yes},
AUTHOR = {S. van Bakel and M. {Dezani-Ciancaglini}},
TITLE = {Characterizing Strong Normalization for Explicit
Substitutions},
BOOKTITLE = {LATIN'02},
YEAR = {2002},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
VOLUME = {2286},
PAGES = {356--370},
ABSTRACT = {
We characterise the strongly normalising terms of a
composition-free
calculus of explicit substitutions (with or without garbage
collection)
by means of an intersection type assignment system.
The main novelty is a new cut-rule which allows to forget
the context
of the minor premise when the context of the main premise
does not have
an assumption for the cut variable.
},
PDF = {http://www.di.unito.it/~dezani/papers/explicit.pdf},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Dez+Ghi:TYPES-2003,
ITRSPAPER = {yes},
AUTHOR = {M. {Dezani-Ciancaglini} and S. Ghilezan},
TITLE = {Two behavioural Lambda models},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
BOOKTITLE = {Types'02},
VOLUME = {2246},
PAGES = {127--147 },
MONTH = {},
YEAR = {2003},
PDF = {http://www.di.unito.it/~dezani/papers/Dg-lncs.pdf},
ABSTRACT = {We build two inverse limit lambda models which characterize
completely sets of terms having similar computational
behaviour. More precisely for each one 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. This is proved by using the finitary logical
description of the models obtained by defining suitable
intersection type assignment systems.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Bar+Bug+Dez+Sas:ASIAN-03,
AUTHOR = {Barbanera, F. and Bugliesi, M. and
Dezani-Ciancaglini, M. and Sassone, V.},
TITLE = {A Calculus of Bounded Capacities},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
BOOKTITLE = {ASIAN'03},
YEAR = 2003,
NUMBER = {2896},
PAGES = {205--223},
NOTE = {},
MONTH = DEC,
PDF = {http://www.di.unito.it/~dezani/papers/asian03.pdf},
ABSTRACT = {Resource control has attracted increasing interest
in foundational research on distributed
systems. This paper focuses on space control and
develops an analysis of space usage in the context
of an ambient-like calculus with bounded capacities
and weighed processes, where migration and
activation require space. A type system complements
the dynamics of the calculus by providing static
guarantees that the intended capacity bounds are
preserved throughout the computation.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Bar+Bug+Dez+Sas:journvers,
AUTHOR = {Barbanera, F. and Bugliesi, M. and
Dezani-Ciancaglini, M. and Sassone, V.},
TITLE = {A Calculus of Bounded Capacities},
YEAR = 2003,
NOTE = {Submitted to a journal. Extendend
version of \cite{Bar+Bug+Dez+Sas:ASIAN-03}},
MONTH = DEC,
PDF = {http://www.di.unito.it/~dezani/papers/bbds.pdf},
ABSTRACT = {Resource control has attracted increasing interest
in foundational research on distributed
systems. This paper focuses on space control and
develops an analysis of space usage in the context
of an ambient-like calculus with bounded capacities
and weighed processes, where migration and
activation require space. A type system complements
the dynamics of the calculus by providing static
guarantees that the intended capacity bounds are
preserved throughout the computation.},
DARTREPORT = {yes}
}
@ARTICLE{Len+Les+Dou+Dez+Bak:IC-2004,
ITRSPAPER = {yes},
AUTHOR = {St{\'e}phane Lengrand and Pierre Lescanne and Daniel J.
Dougherty and Mariangiola Dezani-Ciancaglini and
Steffen van Bakel},
TITLE = {Intersection Types for Explicit Substitutions},
JOURNAL = {Inform.\ {\&} Comput.},
FJOURNAL = {Information and Computation},
VOLUME = 189,
NUMBER = 1,
PAGES = {17--42},
YEAR = 2004,
PDF = {http://www.di.unito.it/~dezani/papers/IaC.pdf},
DARTREPORT = {yes},
ABSTRACT = {We present a new system of intersection types for a
composition-free calculus of explicit substitutions
with a rule for garbage collection, and show that it
characterizes those terms which are strongly
normalizing. This system extends previous work on
the natural generalization of the classical
intersection types system, which characterized head
normalization and weak normalization, but was not
complete for strong normalization. An important role
is played by the notion of \emph{available} variable
in a term, which is a generalization of the
classical notion of free variable.}
}
@ARTICLE{Ale+Dez+Lus:TCS-2003,
AUTHOR = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola and Lusin, Stefania},
TITLE = {Intersection Types and Domain Operators},
JOURNAL = {Theoret.\ Comput.\ Sci.},
FJOURNAL = {Theoretical Computer Science},
NOTE = {to appear},
YEAR = {2003},
MONTH = OCT,
PDF = {http://www.di.unito.it/~dezani/papers/adl.pdf},
DARTREPORT = {yes},
ABSTRACT = {We use intersection types as a tool for obtaining
$\lambda$-models. Relying on the notion of {\em easy intersection
type theory} we successfully build a $\lambda$-model in which the
interpretation of an arbitrary simple easy term is any filter
which can be described by a continuous predicate. This allows us
to prove two results. The first gives a proof of consistency of the $\lambda$-theory where the
$\lambda$-term $(\lambda x.xx)(\lambda x.xx)$ is forced to behave
as the join operator. This result has interesting consequences on
the algebraic structure of the lattice of $\lambda$-theories. The
second result is that for any simple easy term there is a
$\lambda$-model where the interpretation of the term is the {\em
minimal\/} fixed point operator.}
}
@ARTICLE{Dez+Ghi:SI-200X,
ITRSPAPER = {yes},
AUTHOR = {M. {Dezani-Ciancaglini} and S. Ghilezan},
TITLE = {Lambda Models Characterizing Computational
Behaviours of Terms},
JOURNAL = {Schedae Informaticae},
VOLUME = {12},
NUMBER = {},
PAGES = {35--49},
MONTH = {June},
YEAR = {2003},
PDF = {http://www.di.unito.it/~dezani/papers/ScheInfo-I.pdf},
ABSTRACT = {We build a lambda model which characterizes
completely
(persistently) normalizing, (persistently) head
normalizing, and
(persistently) weak head normalizing terms.
This is proved by
using the finitary logical description of the model
obtained
by defining a suitable intersection type assignment
system.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Ale+Lus:ITRS-2002,
ITRSPAPER = {yes},
AUTHOR = {Fabio Alessi and Stefania Lusin},
TITLE = {Simple Easy Terms},
DARTREPORT = {yes},
CROSSREF = {ITRS2002},
ABSTRACT = { We illustrate the use of intersection types as a
semantic
tool for proving easiness result on $lambda$-terms.
We single out the notion of {em simple easiness/} for
$lambda$-terms as a useful semantic property for building
filter models with special purpose features.
Relying on the notion of {em easy intersection type theory},
given
$lambda$-terms $M$ and $E$, with $E$ simple easy,
we successfully build a filter model which equates interpretation
of $M$ and $E$, hence
proving that simple easiness implies easiness.
We finally prove that a class of $lambda$-terms
generated by $omega_2omega_2$ are simple easy,
so providing alternative proof of easiness for them.
},
PDF = {http://www.doc.ic.ac.uk/~svb/ITRS02/ENTCS/entcs75102.pdf},
DEADPDF = {http://www.doc.ic.ac.uk/~svb/ITRS02/ENTCS/AlessiLusin.pdf}
}
@INPROCEEDINGS{Mog+Sab:FICS-2003,
AUTHOR = {E. Moggi and A. Sabry},
TITLE = {An Abstract Monadic Semantics for Value Recursion},
YEAR = 2003,
BOOKTITLE = {FICS'03},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/fics03.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper proposes an operational semantics for value recursion in
the context of monadic metalanguages. Our technique for combining
value recursion with computational effects works \emph{uniformly} for
all monads.
The operational nature of our approach is related to the
implementation of recursion in Scheme and its monadic version proposed
by Friedman and Sabry, but it defines a different semantics and does
not rely on assignments. When contrasted to the axiomatic approach
proposed by Erk\"ok and Launchbury, our semantics for the continuation
monad invalidates one of the axioms, adding to the evidence that this
axiom is problematic in the presence of continuations.
}
}
@ARTICLE{Mog+Sab:AMSVR-03-09,
AUTHOR = {E. Moggi and A. Sabry},
TITLE = {An Abstract Monadic Semantics for Value Recursion},
JOURNAL = {Theoretical Informatics and Applications},
VOLUME = 38,
YEAR = 2004,
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/MS03-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper proposes an operational semantics for value recursion in
the context of monadic metalanguages. Our technique for combining
value recursion with computational effects works \emph{uniformly} for
all monads.
The operational nature of our approach is related to the
implementation of recursion in Scheme and its monadic version proposed
by Friedman and Sabry, but it defines a different semantics and does
not rely on assignments. When contrasted to the axiomatic approach
proposed by Erk\"ok and Launchbury, our semantics for the continuation
monad invalidates one of the axioms, adding to the evidence that this
axiom is problematic in the presence of continuations.
}
}
@ARTICLE{Cal+Mog+She:JFP-ta,
AUTHOR = {C. Calcagno and E. Moggi and T. Sheard},
TITLE = {Closed Types for a Safe Imperative {MetaML}},
JOURNAL = {J.~Funct.\ Programming},
YEAR = {to appear},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/jfp02.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper addresses the issue of safely combining computational
effects and multi-stage programming. We propose a type system,
which
exploits a notion of closed type, to check statically that an
imperative multi-stage program does not cause run-time errors.
Our approach is demonstrated formally for a core language called
$MiniML_{ref}^{meta}$. This core language safely combines
multi-stage
constructs and ML-style references, and is a conservative
extension of
$MiniML_{ref}$, a simple imperative subset of SML.
In previous work, we introduced a closed type constructor,
which was enough to ensure the safe execution of dynamically
generated
code in the pure fragment of $MiniML_{ref}^{meta}$.
}
}
@ARTICLE{Cal+Mog+She:JFP-2003,
AUTHOR = {C. Calcagno and E. Moggi and T. Sheard},
TITLE = {Closed Types for a Safe Imperative {MetaML}},
JOURNAL = {J.~Funct.\ Programming},
VOLUME = 13,
NUMBER = 3,
PAGES = {545--571},
YEAR = {2003},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/jfp02.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper addresses the issue of safely combining computational
effects and multi-stage programming. We propose a type system,
which
exploits a notion of closed type, to check statically that an
imperative multi-stage program does not cause run-time errors.
Our approach is demonstrated formally for a core language called
$MiniML_{ref}^{meta}$. This core language safely combines
multi-stage
constructs and ML-style references, and is a conservative
extension of
$MiniML_{ref}$, a simple imperative subset of SML.
In previous work, we introduced a closed type constructor,
which was enough to ensure the safe execution of dynamically
generated
code in the pure fragment of $MiniML_{ref}^{meta}$.
}
}
@INPROCEEDINGS{Fer+Mog+Pug:FWAN-02,
AUTHOR = {G. Ferrari and E. Moggi and R. Pugliese},
TITLE = {Guardians for Ambient-Based Monitoring},
BOOKTITLE = {{F-WAN}: Foundations of Wide Area Network
Computing},
YEAR = 2002,
SERIES = {ENTCS},
NUMBER = 66,
EDITOR = {V. Sassone},
PUBLISHER = {Elsevier Science},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/fwan02.pdf},
DARTREPORT = {yes},
ABSTRACT = {
In the Mobile Ambients of Cardelli and Gordon an ambient is a
unit for
mobility, which may contain processes (data) and sub-ambients.
Since
the seminal work of Cardelli and Gordon, several ambient-based
calculi
have been proposed (Seal, Box-$\pi$, Safe Ambients, Secure Safe
Ambients, Boxed Ambients), mainly for supporting security. At the
operational level these (box- and) ambient-based calculi differ
only
in the capabilities of processes. We propose a way of extending
ambient-based calculi, which embodies two principles: an ambient
is a
unit for monitoring and coordination, the name of an ambient
determines its (monitoring and coordination) policy.
More specifically, to each ambient we attach a guardian, which
monitors the activity of sub-components (i.e. processes and
sub-ambients) and the interaction with the external
environment. In
our proposal, guardians and processes play a dual role:
guardians are
centralized entities monitoring and inhibiting actions, while
processes are decentralized entities performing actions. We
exemplify
the use of guardians for enforcing security properties.
}
}
@UNPUBLISHED{Fer+Mog+Pug:MetaKlaim-02-11,
AUTHOR = {G. Ferrari and E. Moggi and R. Pugliese},
TITLE = {{MetaKlaim}: A Type Safe Multi-stage Language for
Global Computing},
NOTE = {Submitted},
YEAR = 2002,
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/FMP02-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper describes the design and the semantics of MetaKlaim,
an higher order distributed process calculus equipped with staging
mechanisms.
MetaKlaim integrates MetaML (an extension of SML for
multi-stage programming) and Klaim (a Kernel Language for
Agents Interaction and Mobility), to permit interleaving of
meta-programming activities (like assembly and linking of code
fragments), dynamic checking of security policies at
administrative boundaries and ``traditional'' computational
activities on a wide area network (like remote communication and
code mobility).
MetaKlaim exploits a powerful type system (including polymorphic types a
la system F) to deal with highly parameterized mobile components
and to dynamically enforce security policies: types are metadata
which are extracted from code at run-time and are used to express
trustiness guarantees. The dynamic type checking ensures that the
trustiness guarantees of wide are network applications are
maintained whenever computations interoperate with potentially
untrusted components.
}
}
@ARTICLE{Fer+Mog+Pug:MSCS-ta,
AUTHOR = {G. Ferrari and E. Moggi and R. Pugliese},
TITLE = {{MetaKlaim}: A Type Safe Multi-stage Language for
Global Computing},
JOURNAL = {Math.\ Structures Comput.\ Sci.},
YEAR = {to appear},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/mscs03.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper describes the design and the semantics of MetaKlaim,
an higher order distributed process calculus equipped with staging
mechanisms.
MetaKlaim integrates MetaML (an extension of SML for
multi-stage programming) and Klaim (a Kernel Language for
Agents Interaction and Mobility), to permit interleaving of
meta-programming activities (like assembly and linking of code
fragments), dynamic checking of security policies at
administrative boundaries and ``traditional'' computational
activities on a wide area network (like remote communication and
code mobility).
MetaKlaim exploits a powerful type system (including polymorphic types a
la system F) to deal with highly parameterized mobile components
and to dynamically enforce security policies: types are metadata
which are extracted from code at run-time and are used to express
trustiness guarantees. The dynamic type checking ensures that the
trustiness guarantees of wide are network applications are
maintained whenever computations interoperate with potentially
untrusted components.
}
}
@ARTICLE{Fer+Mog+Pug:MSCS-2004,
AUTHOR = {G. Ferrari and E. Moggi and R. Pugliese},
TITLE = {{MetaKlaim}: A Type Safe Multi-stage Language for
Global Computing},
JOURNAL = {Math.\ Structures Comput.\ Sci.},
YEAR = 2004,
VOLUME = {14},
NUMBER = {3},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/mscs03.pdf},
DARTREPORT = {yes},
ABSTRACT = {
This paper describes the design and the semantics of MetaKlaim,
an higher order distributed process calculus equipped with staging
mechanisms.
MetaKlaim integrates MetaML (an extension of SML for
multi-stage programming) and Klaim (a Kernel Language for
Agents Interaction and Mobility), to permit interleaving of
meta-programming activities (like assembly and linking of code
fragments), dynamic checking of security policies at
administrative boundaries and ``traditional'' computational
activities on a wide area network (like remote communication and
code mobility).
MetaKlaim exploits a powerful type system (including polymorphic types a
la system F) to deal with highly parameterized mobile components
and to dynamically enforce security policies: types are metadata
which are extracted from code at run-time and are used to express
trustiness guarantees. The dynamic type checking ensures that the
trustiness guarantees of wide are network applications are
maintained whenever computations interoperate with potentially
untrusted components.
}
}
@INPROCEEDINGS{Mog+Fag:FOSSACS-2003,
AUTHOR = {E. Moggi and S. Fagorzi},
TITLE = {A Monadic Multi-stage Metalanguage},
CROSSREF = {FOSSACS2003},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/fossacs03.pdf},
DARTREPORT = {yes},
ABSTRACT = {
We describe a metalanguage MMML, which makes explicit the order
of
evaluation (in the spirit of monadic metalanguages) and the
staging of
computations (as in languages for multi-level binding-time
analysis).
The main contribution of the paper is an operational semantics
which
is sufficiently detailed for analyzing subtle aspects of
multi-stage
programming, but also intuitive to serve as a reference
semantics.
For instance, the separation of computational types from code
types,
makes immediate the distinction between a computation for
generating
code and the generated code, and provides a basis for
multi-lingual
extensions, where a variety of programming languages (aka monads)
coexist.
The operational semantics consists of two parts: local (semantic
preserving) simplification rules, and computation steps executed
in a
deterministic order (because they may have side-effects). The
two
parts can be changed independently: the first by adding
datatypes or
recursive definitions, the second by adding other computational
effects. We focus on the computational aspects, thus we adopt a
simple type system, that can detect usual type errors, but not
the
unresolved link errors. Because of its explicit annotations,
MMML is
suitable as an intermediate language, but (in comparison to
MetaML) it
is too verbose as a programming language.
}
}
@UNPUBLISHED{Mog+Fag:MMML-02-10,
AUTHOR = {E. Moggi and S. Fagorzi},
YEAR = 2002,
TITLE = {A Monadic Multi-stage Metalanguage},
NOTE = {Submitted},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/MF02-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
We describe a metalanguage MMML, which makes explicit the order
of
evaluation (in the spirit of monadic metalanguages) and the
staging of
computations (as in languages for multi-level binding-time
analysis).
The main contribution of the paper is an operational semantics
which
is sufficiently detailed for analyzing subtle aspects of
multi-stage
programming, but also intuitive to serve as a reference
semantics.
For instance, the separation of computational types from code
types,
makes immediate the distinction between a computation for
generating
code and the generated code, and provides a basis for
multi-lingual
extensions, where a variety of programming languages (aka monads)
coexist.
The operational semantics consists of two parts: local (semantic
preserving) simplification rules, and computation steps executed
in a
deterministic order (because they may have side-effects). The
two
parts can be changed independently: the first by adding
datatypes or
recursive definitions, the second by adding other computational
effects. We focus on the computational aspects, thus we adopt a
simple type system, that can detect usual type errors, but not
the
unresolved link errors. Because of its explicit annotations,
MMML is
suitable as an intermediate language, but (in comparison to
MetaML) it
is too verbose as a programming language.
}
}
@INPROCEEDINGS{Anc+Fag+Mog+Zuc:ICALP-2003,
AUTHOR = {D. Ancona and S. Fagorzi and E. Moggi and E. Zucca},
TITLE = {Mixin Modules and Computational Effects},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/icalp03.pdf},
DARTREPORT = {yes},
CROSSREF = {ICALP2003},
ABSTRACT = {We define a calculus for investigating the interactions
between mixin modules and computational effects, by combining the
purely functional mixin calculus CMS with a monadic metalanguage
supporting the two separate notions of \emph{simplification} (local rewrite rules)
and \emph{computation} (global evaluation able to modify the store).
This distinction is important for smoothly integrating the CMS rules
(which are all local) with the rules dealing with the imperative features.
In our calculus mixins can contain mutually recursive \emph{computational}
components which are explicitly computed by means of a
new mixin operator whose semantics is defined in terms of a
Haskell-like recursive monadic binding.
Since we mainly focus on the operational aspects, we adopt a simple
type system like that for Haskell, that does not detect dynamic
errors related to bad recursive declarations involving effects.
The calculus serves as a formal basis for defining the semantics of
imperative programming languages supporting first class mixins
while preserving the CMS equational reasoning.}
}
@INPROCEEDINGS{Anc+Fag+Zuc:ICTCS-2003,
AUTHOR = {D. Ancona and S. Fagorzi and E. Zucca},
TITLE = {A Calculus for Dynamic Linking},
PDF = {http://www.disi.unige.it/person/FagorziS/Papers/ICTCS03.pdf},
YEAR = 2003,
DARTREPORT = {yes},
CROSSREF = {ICTCS2003},
PAGES = {284--301},
ABSTRACT = {
We define a calculus for modeling dynamic linking
independently of the details of a particular programming environment.
The calculus distinguishes at the language level the notions of
software configuration and execution, by introducing
separate syntactic notions of linkset expression and command, respectively.
A reduction step can be either a simplification of a linkset
expression, or the execution of a command w.r.t. a specific underlying
software configuration denoted by a linkset expression;
because of dynamic linking, these two kinds of reductions are interleaved.
The type system of the calculus, which is proved to be sound,
relies on an accurate dependency analysis for ensuring type
safety without losing the advantages offered by dynamic linking.}
}
@INPROCEEDINGS{Fag+Zuc+Anc:SAC-2004,
AUTHOR = {S. Fagorzi and E. Zucca and D. Ancona},
TITLE = {Modeling Multiple Class Loaders by a Calculus for Dynamic Linking},
PDF = {http://www.disi.unige.it/person/FagorziS/Papers/OOPS04.pdf},
MONTH = MAR,
DARTREPORT = {yes},
CROSSREF = {SAC-2004},
NOTE = {In OOPS track},
ABSTRACT = {
In a recent paper we proposed a calculus for modeling dynamic linking
independently of the details of a particular programming environment.
Here we use a particular instantiation of this calculus to encode a toy
language, called MCS, which provides an abstract view of the mechanism of
dynamic class loading with multiple loaders as in Java.
The aim is twofold. On one hand, we show an example of application of
the calculus in modeling existing
loading and linking policies, showing in particular that Java-like loading
with multiple loaders can be
encoded without exploiting the full expressive power of the calculus.
On the other hand, we provide a simple formal model which allows a better
understanding of Java-like
loading mechanisms and also shows an intermediate solution between the rigid
approach based only on
the class path and that which allows arbitrary user-defined loaders,
which can be intricate and error-prone.}
}
@INPROCEEDINGS{Anc+Fag+Zuc:TCS2004,
AUTHOR = {Davide Ancona and Sonia Fagorzi and Elena Zucca},
TITLE = {A Calculus with Lazy Module Operators},
CROSSREF = {TCS2004},
PAGES = {423--436},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TCS04.pdf},
DARTREPORT = {yes},
ABSTRACT = {Modern programming environments such as those of
Java and C\# support dynamic loading of software
fragments. More in general, we can expect that in
the future systems will support more and more forms
of interleaving of \emph{reconfiguration} steps and
standard \emph{execution} steps, where the software
fragments composing a program are dynamically
changed and/or combined on demand and in different
ways. However, existing kernel calculi providing
formal foundations for module systems are based on a
\emph{static} view of module manipulation, in the
sense that open code fragments can be flexibly
combined together, but all module operators must be
performed once for all \emph{before} starting
execution of a program, that is, evaluation of a
module component. The definition of clean and
powerful module calculi supporting \emph{lazy}
module operators, that is, operators which can be
performed \emph{after\/} the selection of some
module component, is still an open problem. Here, we
provide an example in this direction (the first at
our knowledge), defining ${\it CMS}^{\ell}$, an
extension of the Calculus of Module Systems
\cite{Anc+Zuc:JFP-2002} where module operators can
be performed at execution time and, in particular,
are executed on demand, that is, only when needed by
the executing program. In other words, execution
steps, if possible, take the precedence over
reconfiguration steps. The type system of the
calculus, which is proved to be sound, relies on a
dependency analysis which ensures that execution
will never try to access module components which
cannot become available by performing
reconfiguration steps.}
}
@INPROCEEDINGS{Anc+Fag+Zuc:WOOD-2004,
AUTHOR = {D.~Ancona and S.~Fagorzi and E.~Zucca},
TITLE = {A Calculus for Dynamic Reconfiguration with Low Priority Linking},
BOOKTITLE = {Workshop on Object-Oriented Developments 2004},
YEAR = 2004,
MONTH = AUG,
SERIES = {ENTCS},
PUBLISHER = {Elsevier},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/WOOD04.pdf},
NOTE = {To appear},
DARTREPORT = {yes},
ABSTRACT = {
Building on our previous work, we present a simple module calculus where execution steps of a module component can be interleaved with reconfiguration steps (that is, reductions at the module level), and where execution can partly control precedence between these reconfiguration steps.
This is achieved by means of a \emph{low priority link\/} operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples.
We ensure soundness by combining a static type system, which prevents errors in applying module operators, and a dynamic check which raises a linkage error if the running program needs a component which cannot be provided by reconfiguration steps. In particular no linkage errors can be raised if \emph{all} components are potentially available.
}
}
@INPROCEEDINGS{Anc+Fag+Zuc:TGC-2005,
AUTHOR = {D.~Ancona and S.~Fagorzi and E.~Zucca},
TITLE = {Mixin Modules for Dynamic Rebinding},
BOOKTITLE = {TGC 2005 - Symposium on Trustworthy Global Computing},
YEAR = 2005,
MONTH = APR,
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
DOCUMENTURL = {http://www.disi.unige.it/person/AnconaD/Conferences.html#AnconaEtAl05},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TGC05.pdf},
NOTE = {To appear},
DARTREPORT = {yes},
ABSTRACT = {
\emph{Dynamic rebinding} is the ability of changing the definitions of names at execution time.
While dynamic rebinding is clearly useful in practice, and increasingly needed in modern systems, most programming
languages provide only limited and ad-hoc mechanisms, and no adequate semantic understanding currently exists.
Here, we provide a simple and powerful mechanism for dynamic rebinding by means of a calculus CMS^{l,v} of
\emph{mixin modules} (mutually recursive modules allowing redefinition of components) where, differently from the
traditional approach, module operations can be performed {after selecting and executing} a module component:
in this way, execution can refer to \emph{virtual} components, which can be rebound when module operators are executed.
In particular, in our calculus module operations are performed on demand, when execution would otherwise get stuck.
We provide a sound type system, which ensures that execution never tries to access module components which cannot become available, and show how the calculus can be used to encode a variety of real-world dynamic rebinding mechanisms.
}
}
@ARTICLE{Fag+Zuc:JOT-2004-v3n11,
AUTHOR = {S.~Fagorzi and E.~Zucca},
TITLE = {A Case-Study in Encoding Configuration Languages: Multiple Class Loaders},
JOURNAL = {Journal of Object Technology},
YEAR = 2004,
MONTH = DEC,
VOLUME = 3,
NUMBER = 11,
PAGES = {31--53},
PUBLISHER = {Chair of Software Engineering (ETH Zurich)},
PDF = {http://www.jot.fm/issues/issue_2004_12/article2/article2.pdf},
DARTREPORT = {yes},
ABSTRACT = {
The contribution of the paper is twofold.
First, we define a toy language, called MCL, which provides a very abstract view of the mechanism
of dynamic class loading with multiple loaders as in Java. The aim is to study this feature in isolation,
allowing a better understanding; moreover, this also shows a stratified approach, which,
differently from the Java approach based on reflection, distinguishes between the language at the
user level and the configuration language. This approach is less flexible but allows to statically
check type safety, hence provides an intermediate solution between the rigid approach based only on
the class path and that which allows loaders to depend on execution of user applications,
which can be intricate and error-prone.
The second contribution is related to a recent stream of work aiming at defining simple and powerful
calculi providing a common foundation for systems supporting dynamic reconfiguration. We use MCL as
an extended case-study, by defining an encoding in one of these kernel calculi, and prove
the correctness of the translation.}
}
@ARTICLE{Lag:JOT-2004-v3n11,
AUTHOR = {G.~Lagorio},
TITLE = {Capturing ghost dependencies in {J}ava sources},
JOURNAL = {Journal of Object Technology},
YEAR = 2004,
MONTH = DEC,
VOLUME = 3,
NUMBER = 11,
PAGES = {77--95},
PUBLISHER = {Chair of Software Engineering (ETH Zurich)},
PDF = {http://www.jot.fm/issues/issue_2004_12/article4/article4.pdf},
DARTREPORT = {yes},
ABSTRACT = {
All non trivial applications consist of many sources, which
usually depend on each other. For this reason, a change to some sources may
affect the compilation of other (unchanged) sources.
Hence, the recompilation must be propagated to the unchanged sources
that \emph{depend} on the changed ones, in order to obtain the same result
a global recompilation would produce.
Most IDEs (Integrated Development Environments) provide
\emph{smart} dependency checking; that is, they automate the task
of finding these dependencies and propagating the
recompilation when an application is rebuilt.
In this paper we study the problem of extracting dependency information
from Java sources and
propose an encoding of
these dependency information as regular expressions. This
encoding is both compact to store and fast to check.
Furthermore, our technique detects
a particular kind of dependencies, which we call \emph{ghost dependencies},
that popular tools, even commercial ones, fail to detect.
Because of this failure, some required recompilations are not triggered by
these tools and the result of their incremental recompilations is
not equivalent to the recompilation of all sources.
}
}
@UNPUBLISHED{Anc+Mog:CSNM-03-10,
AUTHOR = {D. Ancona and E. Moggi},
TITLE = {A Calculus for Symbolic Names Management},
YEAR = 2003,
NOTE = {Submitted},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/AM03-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
We define a basic calculus $ML^N$ for manipulating symbolic names
inspired by both the $\nu^Box$ calculus of Nanevski and Pfenning and
the $CMS$ calculus of Ancona and Zucca. The resulting calculus
provides a smooth integration of the peculiar features of $\nu^Box$ and
$CMS$, namely the use of symbolic names for meta-programming and
programming in-the-large, and overcomes several deficiencies of these
two calculi.
We present two different extensions of the basic calculus, the first
consider the interaction between linking and computational effects (in
the form of imperative computations), the second shows how $CMS$ can
be naturally encoded into $ML^N$.
A posteriori the calculus appears related to $\lambda$-calculi with
extensible records, and able to model some aspects of the mechanism of
Java class loaders.
}
}
@INPROCEEDINGS{Anc+Mog:GPCE-2004,
AUTHOR = {D. Ancona and E. Moggi},
TITLE = {A Fresh Calculus for Names Management},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/gpce04.pdf},
DARTREPORT = {yes},
CROSSREF = {GPCE2004},
ABSTRACT = {
We define a basic calculus $ML^N$ for manipulating symbolic names
inspired by both the $\nu^Box$ calculus of Nanevski and Pfenning and
the $CMS$ calculus of Ancona and Zucca. The resulting calculus
provides a smooth integration of the peculiar features of $\nu^Box$ and
$CMS$, namely the use of symbolic names for meta-programming and
programming in-the-large, and overcomes several deficiencies of these
two calculi.
We present two different extensions of the basic calculus, the first
consider the interaction between linking and computational effects (in
the form of imperative computations), the second shows how $CMS$ can
be naturally encoded into $ML^N$.
A posteriori the calculus appears related to $\lambda$-calculi with
extensible records, and able to model some aspects of the mechanism of
Java class loaders.
}
}
@INPROCEEDINGS{Anc+Mog:FMCO-2004,
AUTHOR = {D. Ancona and E. Moggi},
TITLE = {Program Generation and Components},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/fmco04.pdf},
DARTREPORT = {yes},
EDITOR = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf},
BOOKTITLE = {Formal Methods for Components and Objects: Third
International Symposium, FMCO 2004, Leiden, The
Netherlands, November 2--5, 2004. Revised Lectures},
VOLUME = {3167},
PUBLISHER = {Springer-Verlag},
YEAR = {2005},
SERIES = {LNCS},
ABSTRACT = {
The first part of the paper gives a brief overview of meta-programming,
in particular program generation, and its use in software development.
The second part introduces a basic calculus, related to FreshML, that
supports program generation (as described through examples and a
translation of MetaML into it) and programming in-the-large (this is
demonstrated by a translation of CMS into it).
}
}
@UNPUBLISHED{Mog:CMM-04-01,
AUTHOR = {E. Moggi},
TITLE = {A Cumulative Monadic Metalanguage},
YEAR = 2004,
NOTE = {Unpublished},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/Mog-CMM.pdf},
DARTREPORT = {yes},
ABSTRACT = {We introduce a monadic metalanguage which combines two previously
proposed monadic metalanguages: one for staging and the other for
value recursion. The metalanguage includes also extensible records
a basic name management facility.}
}
@UNPUBLISHED{Cal+Mog+Tah:MLIC-03-10,
AUTHOR = {C. Calcagno and E. Moggi and W. Taha},
TITLE = {{ML}-like Inference for Classifiers},
YEAR = 2003,
NOTE = {Accepted to ESOP'04},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/CMT03-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
Environment classifiers were recently proposed as a new approach to
typing multi-stage languages. Safety was established in the
simply-typed and let-polymorphic settings. While the motivation
for the classifier approach was the feasibility of inference, this was
in fact not established.
This paper starts with the observation that inference for the full
classifier-based system fails. We then identify a subset of the
original system for which inference is possible.
This subset, which uses {implicit classifiers}, retains
significant expressivity (e.g. it can embed the calculi of Davies and
Pfenning) and eliminates the need for classifier names in terms.
Implicit classifiers were implemented in MetaOCaml, and no changes
were needed to make an existing test suite acceptable by the new type
checker.
}
}
@INPROCEEDINGS{Cal+Mog+Tah:ESOP-2004,
AUTHOR = {C. Calcagno and E. Moggi and W. Taha},
TITLE = {{ML}-like Inference for Classifiers},
CROSSREF = {ESOP2004},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/CMT03-sub.pdf},
DARTREPORT = {yes},
ABSTRACT = {
Environment classifiers were recently proposed as a new approach to
typing multi-stage languages. Safety was established in the
simply-typed and let-polymorphic settings. While the motivation
for the classifier approach was the feasibility of inference, this was
in fact not established.
This paper starts with the observation that inference for the full
classifier-based system fails. We then identify a subset of the
original system for which inference is possible.
This subset, which uses {implicit classifiers}, retains
significant expressivity (e.g. it can embed the calculi of Davies and
Pfenning) and eliminates the need for classifier names in terms.
Implicit classifiers were implemented in MetaOCaml, and no changes
were needed to make an existing test suite acceptable by the new type
checker.
}
}
@INPROCEEDINGS{Mic+Sca:PPDP-2003,
AUTHOR = {Marino Miculan and Ivan Scagnetto},
TITLE = {A Framework for Typed {HOAS} and Semantics},
CROSSREF = {PPDP2003},
DARTREPORT = {yes},
PDF = {http://www.dimi.uniud.it/~miculan/Papers/PPDP03.pdf},
ABSTRACT = {We investigate a framework for representing and
reasoning about syntactic and semantic aspects of typed languages
with variable binders.
First, we introduce \emph{typed binding signatures} and develop a
theory of typed abstract syntax with binders. Each signature is
associated to a category of ``presentation'' models, where the
language of the typed signature is the initial model.
At the semantic level, types can be given also a computational
meaning in a (possibly different) \emph{semantic} category. We
observe that in general, semantic aspects of terms and variables can
be reflected in the presentation category by means of an adjunction.
Therefore, the category of presentation models is expressive enough
to represent both the syntactic and the semantic aspects of
languages.
We introduce then a \emph{meta}logical system, inspired by the
internal languages of the presentation category, which can be used
for reasoning on both the syntax and the semantics of languages.
This system is composed by a core equational logic tailored for
reasoning on the syntactic aspects; when a specific semantics is
chosen, the system can be modularly extended with further
``semantic'' notions, as needed.}
}
@INPROCEEDINGS{Mar+Zac:COMETA-2003,
MAYBEITRSPAPER = {yes???},
AUTHOR = {Ines Margaria and Maddalena Zacchi},
TITLE = {A Filter Model for Safe Ambients},
CROSSREF = {COMETA2003},
PDF = {http://www.di.unito.it/~ines/papers/fmsa.pdf},
DARTREPORT = {yes},
ABSTRACT = {
The definition of filter model is extended to a variant of Ambient
Calculus:
Safe Ambient Calculus, introduced for developing an algebraic theory for
a bisimulation-based behavioral equivalence.
The types are constructed by means
of elementary and higher-order actions,
that define the moves processes can do.
Entailment rules for types allow to translate the parallel
composition of moves
into nondeterministic choice of sequences of interleaved actions,
providing a normal form
for types assigned to processes.
In the filter model obtained via the introduced
type system, any process is interpreted as the set of all its types.
The type assignment system results to be sound and complete with respect
to the given semantics.
Moreover the partial order relation induced by the filter
model is compared with observational equivalence:
the model is proved adequate,
but it is shown, by means of a counter-example, that full abstractness fails.}
}
@INPROCEEDINGS{Damiani:PPDP-2003,
ITRSPAPER = {yes},
TITLE = {Rank 2 Intersection Types for Modules},
AUTHOR = {F. Damiani},
CROSSREF = {PPDP2003},
PAGES = {67--78},
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/ppdp03.html},
PDF = {http://www.di.unito.it/~damiani/papers/ppdp03.pdf},
DARTREPORT = {yes},
ABSTRACT = {We
present a rank 2 intersection type system for a language of modules built
on a core ML-like language. The {\em principal typing property} of the rank
2 intersection type system for the core language plays a crucial role in the
design of the type system for the module language. We first considers a
``plain'' notion of module, where a module is just a set of mutually recursive
top-level definitions, and illustrates the notions of:
{\em module intrachecking} (each module is typechecked in isolation and its
interface, that is the set of typings of the defined identifiers,
is inferred);
{\em interface interchecking}
(when linking modules, typechecking is done just by looking at the interfaces);
{\em interface specialization} (interface intrachecking may require to
specialize the typing listed in the interfaces);
{\em principal interfaces} (the principal typing property for the type system
of modules);
and {\em separate typechecking} (looking at the code of the modules does not
provide more type information than looking at their interfaces).
Then we illustrate some limitations of the ``plain'' framework and extend the
module language and the type system in order to overcome these limitations.
The decidability of the system is shown by providing
algorithms for the fundamental operations involved in module intrachecking
and interface interchecking.}
}
@INPROCEEDINGS{Damiani+Drossopoulou+Giannini:ICTCS-03,
AUTHOR = {F. Damiani and S. Drossopoulou and P. Giannini},
TITLE = {Refined Effects for Unanticipated Object Re-classification:
Fickle3 (Extended Abstract)},
BOOKTITLE = {ICTCS'03},
YEAR = {2003},
PUBLISHER = {Springer},
PAGES = {97--110},
SERIES = {LNCS},
VOLUME = 2841,
ABSTRACT = {
In previous work with Dezani on the language Fickle and its extension FickleII
we introduced language features for object re-classification for imperative,
typed, class-based, object-oriented languages.
In this paper we present the language Fickle3, which on one side refines
FickleII with more expressive effect annotations, and on the other eliminates
the need to declare explicitly which are the classes of the objects that may
be re-classified. Therefore, Ficle3 allows to correctly type meaningful
programs which FickleII rejects. Moreover, re-classification may be decided by
the client of a class, allowing ``unanticipated object re-classification''.
As for FickleII, also the type and effect system for Fickle3 guarantees that,
even though objects may be re-classified across classes with different
members, they will never attempt to access non existing members.
The type and effect system of Fickle3 has some significant differences from
the one of FickleII. In particular, besides the fact that intra-class type
checking has to track the more refined effects, when a class is combined with
other classes some additional inter-class checking is introduced.
},
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/ictcs03.html},
PDF = {http://www.di.unito.it/~damiani/papers/ictcs03.pdf},
DARTREPORT = {yes}
}
@UNPUBLISHED{Damiani:2003b,
ITRSPAPER = {yes},
TITLE = {Principal Typings and True Rank 2 Intersection Typable Recursive
Definitions},
AUTHOR = {F. Damiani},
YEAR = {2003},
MONTH = OCT,
NOTE = {Internal report. Superseded by~\cite{Damiani:TLCA-05-ExtVer}},
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/recp2.html},
PDF = {http://www.di.unito.it/~damiani/papers/recp2.pdf},
ABSTRACT = {
We propose new typing rules for assigning rank 2 intersection
types to (possibly mutually) recursive definitions. A major
achievement of the new rules over previous proposals is that they
allow to type also {\em true rank 2 intersection typable}
recursive definitions (i.e., recursive definitions that have a
rank 2 intersection type and no simple type). A notable feature of
these rules is that they rely entirely on the {\em principal
typing property}, so they can be added to any system with
principal typings.
},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Cardone+Coppo:ICTCS-03,
AUTHOR = {M. Coppo and F. Cardone},
TITLE = {Decidability Properties of Recursive Types},
BOOKTITLE = {ICTCS'03},
YEAR = {2003},
PUBLISHER = {Springer-Verlag},
PAGES = {242--255},
SERIES = {LNCS},
VOLUME = 2841,
ABSTRACT = {
In this paper we study decision problems and invertibility for
two notions of equivalence of recursive types. In particular,
for recursive types presented by means of a recursion operator $\mu$,
we describe an algorithm showing that the natural equivalence generated
by finitely many steps of folding and unfolding of $\mu$-types is
decidable. For recursive types presented by finite systems of recursive
equations, we give a thoroughly coinductive characterization of the
equivalence induced by their interpretation as infinite (regular)
trees, from which the decidability of this equivalence follows.
A formal proof of the former result, to our knowledge, has never
appeared in the literature. The latter result, on the contrary,
is well known but we present here a new proof obtained as an
application of general coalgebraic facts to the theory of recursive
types. From these results invertibility is easily proved
for both equivalences.},
PDF = {http://www.di.unito.it/~coppo/papers/ICTCS03.pdf},
DARTREPORT = {yes}
}
@UNPUBLISHED{Damiani:2003,
TITLE = {Rank 2 {I}ntersection {T}ypes for {M}odules},
AUTHOR = {F. Damiani},
YEAR = {2003},
MONTH = JUN,
NOTE = {Version with conclusions and appendices
of~\cite{Damiani:PPDP-2003}},
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/ppdp03.html},
PDF = {http://www.di.unito.it/~damiani/papers/ppdp03wCaA.pdf},
ABSTRACT = {We
present a rank 2 intersection type system for a language of modules built
on a core ML-like language. The {\em principal typing property} of the rank
2 intersection type system for the core language plays a crucial role in the
design of the type system for the module language. We first considers a
``plain'' notion of module, where a module is just a set of mutually recursive
top-level definitions, and illustrates the notions of:
{\em module intrachecking} (each module is typechecked in isolation and its
interface, that is the set of typings of the defined identifiers,
is inferred);
{\em interface interchecking}
(when linking modules, typechecking is done just by looking at the interfaces);
{\em interface specialization} (interface intrachecking may require to
specialize the typing listed in the interfaces);
{\em principal interfaces} (the principal typing property for the type system
of modules);
and {\em separate typechecking} (looking at the code of the modules does not
provide more type information than looking at their interfaces).
Then we illustrate some limitations of the ``plain'' framework and extend the
module language and the type system in order to overcome these limitations.
The decidability of the system is shown by providing
algorithms for the fundamental operations involved in module intrachecking
and interface interchecking.},
DARTREPORT = {yes}
}
@UNPUBLISHED{Cop+Gio:03,
AUTHOR = {Coppo, M. and Giovannetti, E.},
TITLE = {Prolog implementation of type inference algorithms
for mobile ambients},
MONTH = JUN,
YEAR = 2003,
NOTE = {Internal report},
DARTREPORT = {yes},
PDF = {http://www.macs.hw.ac.uk/DART/reports/D2.2/CG03.pdf},
ABSTRACT = {
}
}
@INPROCEEDINGS{Anc+Zuc:POPL-2004,
AUTHOR = {Davide Ancona and Elena Zucca},
TITLE = {Principal Typings for {J}ava-like Languages},
CROSSREF = {POPL2004},
DARTREPORT = {yes},
POSTSCRIPT = {ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL04.ps.gz},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL04.pdf},
DOCUMENTURL = {http://www.disi.unige.it/person/ZuccaE/Research/PublicationData.html#AnconaZucca03},
ABSTRACT = {The contribution of the paper is twofold. First, we provide a general notion of type system supporting separate compilation and inter-checking, and a formal definition of soundess and completeness of inter-checking w.r.t. global compilation. These properties are important in practice since they allow selective recompilation. In particular, we show that they are guaranteed when the type system has principal typings and provides sound and complete entailment relation between type environments and types.
The second contribution is more specific, and is an instantiation of the notion of type system previously defined for Featherweight Java [IgarashiEtAl@OOPSLA99] with method overloading and field hiding. The aim is to show that it is possible to define type systems for Java-like languages, which, differently from those used by standard compilers, have principal typings, hence can be used as a basis for selective recompilation.
},
YEAR = 2004
}
@INPROCEEDINGS{Anc+Dam+Dro+Zuc:POPL-2005,
AUTHOR = {D.~Ancona and F.~Damiani and S.~Drossopoulou and E.~Zucca},
TITLE = {Polymorphic Bytecode: Compositional
Compilation for {J}ava-like Languages},
CROSSREF = {POPL2005},
PAGES = {26--37},
DARTREPORT = {yes},
DOCUMENTURL = {http://www.disi.unige.it/person/ZuccaE/Research/PublicationData.html#AnconaEtAl04},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL05.pdf},
ABSTRACT = {We define compositional compilation as
the ability to typecheck source code fragments in
isolation, generate corresponding binaries, and link together
fragments whose mutual assumptions are satisfied, without
reinspecting the code. Even though compositional compilation is a
highly desirable feature,
in Java-like languages it can hardly be achieved. This is due to
the fact that the bytecode generated for a fragment (say, a class)
is not uniquely determined by its source code, but also
depends on the compilation context.
We propose
a way to obtain compositional compilation for Java, by introducing
a polymorphic form of bytecode containing type variables
(ranging over class names) and equipped with a set of constraints
involving type variables. Thus,
polymorphic bytecode provides a representation for all the
(standard) bytecode
that can be obtained by replacing
type variables with classes
satisfying the associated constraints.
We illustrate our proposal by developing a typing and a
linking algorithm. The
typing
algorithm compiles a class in isolation generating the
corresponding polymorphic bytecode fragment and
constraints on the classes it depends on. The linking algorithm
takes a collection of polymorphic bytecode fragments, checks their
mutual consistency, and possibly simplifies and specializes them. In
particular, linking a self-contained collection of fragments
either fails, or produces standard bytecode
(the same as what
would have been produced by standard compilation of
all fragments).}
}
@UNPUBLISHED{Anc+Dam+Dro+Zuc:CCfJLtPB-2005,
AUTHOR = {D.~Ancona and F.~Damiani and S.~Drossopoulou and E.~Zucca},
TITLE = {Compositional
Compilation for {J}ava-like Languages through Polymorphic Bytecode},
DARTREPORT = {yes},
YEAR = {2005},
MONTH = {January},
NOTE = {Extended version of \cite{Anc+Dam+Dro+Zuc:POPL-2005} with proofs},
DOCUMENTURL = {http://www.disi.unige.it/person/AnconaD/Reports.html#AnconaEtAl05c},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PBCCJL.pdf},
ABSTRACT = {
We define compositional compilation as
the ability to typecheck source code fragments in
isolation, generate corresponding binaries, and link together
fragments whose mutual assumptions are satisfied, without
reinspecting the code. Even though compositional compilation is a
highly desirable feature,
in Java-like languages it can hardly be achieved. This is due to
the fact that the bytecode generated for a fragment (say, a class)
is not uniquely determined by its source code, but also
depends on the compilation context.
We propose
a way to obtain compositional compilation for Java, by introducing
a polymorphic form of bytecode containing type variables
(ranging over class names) and equipped with a set of constraints
involving type variables. Thus,
polymorphic bytecode provides a representation for all the
(standard) bytecode
that can be obtained by replacing
type variables with classes satisfying the associated constraints.
We illustrate our proposal by developing a typing and a
linking algorithm. The typing
algorithm compiles a class in isolation generating the
corresponding polymorphic bytecode fragment and
constraints on the classes it depends on. The linking algorithm
takes a collection of polymorphic bytecode fragments, checks their
mutual consistency, and possibly simplifies and specializes them. In
particular, linking a self-contained collection of fragments
either fails, or produces standard bytecode
(the same as what would have been produced by standard compilation of
all fragments).
}
}
@INPROCEEDINGS{Giovannetti:tutorial,
AUTHOR = {E. Giovannetti},
TITLE = {Ambient Calculi with Types: a Tutorial},
BOOKTITLE = {Global {C}omputing - {P}rogramming {E}nvironments, {L}anguages,
{S}ecurity and {A}nalysis of {S}ystems},
PUBLISHER = {Springer-Verlag},
YEAR = {2003},
SERIES = {LNCS},
VOLUME = {2874},
PDF = {http://www.di.unito.it/~elio/papers/elio-trento.pdf},
ABSTRACT = {A tutorial introduction to the key concepts of ambient calculi and
their type disciplines, illustrated through a number
of systems proposed in the last few years, such as Mobile Ambients,
Safe Ambients, Boxed Ambients, and other related calculi with types.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{Gio:CATS-2004,
AUTHOR = {E. Giovannetti},
TITLE = {Type Inference for {M}obile {A}mbients in {P}rolog},
BOOKTITLE = {CATS 2004},
YEAR = {2004},
ABSTRACT = {The type system for the ambient calculus $\mathrm{M}^3$
is presented in a new form
that derives the type of a term with the minimal set of mobility assumptions,
and is therefore more amenable than the original form to
a translation into a type inference algorithm.
From the new formulation a Prolog program is derived, which
implements a type inference algorithm for $\mathrm{M}^3$ analogous
to the one previously specified through formal rules.
The implementation exploits in the standard way
the peculiarities of the logic programming paradigm,
and is therefore, in a sense, more abstract than the
original algorithm's specification itself.},
SERIES = {ENTCS},
VOLUME = {91},
PAGES = {96--115},
PDF = {http://www.di.unito.it/~elio/papers/cats04.pdf},
DARTREPORT = {yes}
}
@ARTICLE{Dez+Mey+Mot:NDJFL-02,
ITRSPAPER = {yes},
AUTHOR = {Mariangiola Dezani and Robert Meyer and Yoko
Motohama},
TITLE = {The semantics of entailment omega},
JOURNAL = {Notre Dame J.~Formal Logic},
YEAR = 2002,
VOLUME = 43,
NUMBER = 3,
PAGES = {129--145},
PDF = {http://www.di.unito.it/~dezani/papers/ndj03.pdf},
ABSTRACT = {
This paper discusses the relation between the minimal positive relevant
logic ${\bf B}$+ and intersection and union type theories. There is a
marvellous coincidence between these very differently motivated research
areas. First, we show a perfect fit between the Intersection Type
Discipline {\bf ITD} and the tweaking ${\bf B\land T}$ of ${\bf B}$+,
which saves implication $\to$ and conjunction $\land$ but drops
disjunction $\lor$. The {\em filter models} of the
$\lambda$-calculus (and its intimate partner Combinatory Logic {\bf
CL}) of the first author and her co-authors then become {\em theory
models} of these calculi. (The logician's {\em Theory} is the algebraist's
{\em Filter}.) The coincidence extends to a dual interpretation of key
particles -- the subtype $\leq$ translates to provable $\to$, type intersection $\cap$ to conjunction
$\land$, function space $\to$ to implication and whole domain $\omega$
to the (trivially added but trivial) truth {\bf T}. This satisfying
ointment contains a fly. For it is right, proper and to be expected
that type union $\cup$ should correspond to the logical disjunction
$\lor$ of ${\bf B}$+. But the simulation of functional application by a
fusion (or modus ponens product) operation $\circ$ on theories leaves
the key {\em Bubbling lemma} of work on {\bf ITD} unprovable for the
{\em $\lor$-prime theories} now appropriate for the modelling. The focus
of the present paper lies in an appeal to {\em Harrop theories} which
are (a) prime and (b) closed under fusion. A version of the Bubbling
lemma is then proved for Harrop theories, which accordingly furnish a
model of $\lambda$ and {\bf CL}.},
DARTREPORT = {yes}
}
@ARTICLE{Dez:BSL-2003,
DARTREPORT = {yes},
ITRSPAPER = {yes},
TITLE = {Finitary Logical Semantics (abstract)},
AUTHOR = {M. Dezani},
JOURNAL = {The Bulletin of Symbolic Logic},
YEAR = {2003},
PAGES = {257--258},
VOLUME = {9},
NUMBER = {2},
PDF = {http://www.di.unito.it/~dezani/papers/abstLS.pdf}
}
@ARTICLE{Dez+Ghi+Lik:TCS-2004,
ITRSPAPER = {yes},
AUTHOR = {Dezani-Ciancaglini, Mariangiola and Ghilezan, Silvia
and Likavec, Silvia},
TITLE = {Behavioural Inverse Limit $\lambda$-Models},
JOURNAL = {Theoret.\ Comput.\ Sci.},
VOLUME = 316,
NUMBER = {1--3},
PAGES = {49--74},
YEAR = 2004,
PDF = {http://www.di.unito.it/~dezani/papers/dgl.pdf},
DARTREPORT = {yes},
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.}
}
@ARTICLE{Ale+Dez+Lus:TCS-2004,
ITRSPAPER = {yes},
AUTHOR = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola
and Lusin, Stefania},
TITLE = {Intersection Types and Domain Operators},
JOURNAL = {Theoret.\ Comput.\ Sci.},
FJOURNAL = {Theoretical Compututer Science},
VOLUME = 316,
NUMBER = {1--3},
PAGES = {25--47},
YEAR = 2004,
PDF = {http://www.di.unito.it/~dezani/papers/adl.pdf},
DARTREPORT = {yes},
ABSTRACT = {We use intersection types as a tool for obtaining
$\lambda$-models. Relying on the notion of {\em easy
intersection type theory} we successfully build a
$\lambda$-model in which the interpretation of an
arbitrary simple easy term is any filter which can
be described by a continuous predicate. This allows
us to prove two results. The first gives a proof of
consistency of the $\lambda$-theory where the
$\lambda$-term $(\lambda x.xx)(\lambda x.xx)$ is
forced to behave as the join operator. This result
has interesting consequences on the algebraic
structure of the lattice of $\lambda$-theories. The
second result is that for any simple easy term there
is a $\lambda$-model where the interpretation of the
term is the \emph{minimal} fixed point operator.}
}
@ARTICLE{alesbarbdeza05,
AUTHOR = {Alessi, Fabio and Barbanera, Franco and
Dezani-Ciancaglini, Mariangiola},
TITLE = {Intersection Types and Lambda Models},
JOURNAL = {Theoret.\ Comput.\ Sci.},
FJOURNAL = {Theoretical Compututer Science},
YEAR = 2005,
NOTE = {to appear},
PDF = {http://www.di.unito.it/~dezani/papers/abdtcs.pdf},
DARTREPORT = {yes},
ABSTRACT = {Invariance of interpretation by $\beta$-conversion is one of the minimal requirements
for any standard model for the $\lambda$-calculus.
With the intersection type systems being a general framework for the study of
semantic domains for the $\lambda$-calculus, the present paper provides
a (syntactic) characterisation of the above mentioned requirement in terms of
characterisation results for intersection type assignment systems.
Instead of considering conversion as a whole, reduction and expansion
will be considered separately. Not only for usual computational rules
like $\beta$, $\eta$, but also for a number of relevant restrictions of those.
Characterisations will be also provided for (intersection) filter
structures that are indeed $\lambda$-models.}
}
@INPROCEEDINGS{alesbarbdeza04,
ITRSPAPER = {yes},
AUTHOR = {Alessi, Fabio and Barbanera, Franco and
Dezani-Ciancaglini, Mariangiola},
TITLE = {Tailoring Filter Models},
BOOKTITLE = {Types '03},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
PAGES = {17--33},
YEAR = 2004,
VOLUME = 3085,
EDITOR = {Stefano Berardi and Mario Coppo and Ferruccio
Damiani},
PDF = {http://www.di.unito.it/~dezani/papers/abd.pdf},
DARTREPORT = {yes},
ABSTRACT = {Conditions on type preorders are provided in order
to characterize the induced filter models for the
$\lambda$-calculus and some of its
restrictions. Besides, two examples are given of
filter models in which not all the continuous
functions are representable.}
}
@INPROCEEDINGS{alesdeza04,
ITRSPAPER = {yes},
AUTHOR = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola},
TITLE = {Type preorders and recursive terms},
CROSSREF = {ITRS2004},
PAGES = {3--21},
PDF = {http://www.di.unito.it/~dezani/papers/ad.pdf},
DARTREPORT = {yes},
ABSTRACT = {We show how to use intersection types for building
models of a $\lambda$-calculus enriched with
recursive terms, whose intended meaning is of
\emph{minimal} fixed points. As a by-product we
prove an interesting consistency result.}
}
@INPROCEEDINGS{alesdezahons04,
ITRSPAPER = {yes},
AUTHOR = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola
and Honsell, Furio},
TITLE = {Inverse Limit Models as Filter Models},
BOOKTITLE = {HOR '04},
PAGES = {3--25},
YEAR = 2004,
EDITOR = {Delia Kesner and Femke van Raamsdonk and
J. B. Wells},
XNOTE = {ISSN 0935-3232, AIB-2004- 03},
PUBLISHER = {RWTH Aachen},
ADDRESS = {Aachen},
PDF = {http://www.di.unito.it/~dezani/papers/adh.pdf},
DARTREPORT = {yes},
ABSTRACT = {Natural intersection type preorders are the type
structures which agree with the plain intuition of
intersection type constructor as set-theoretic
intersection operation and arrow type constructor as
set-theoretic function space constructor. In this
paper we study the relation between natural
intersection type preorders and natural
$\lambda$-structures, i.e. $\omega$-algebraic
lattices $\D$ with Galois connections given by
$F:\D\rightarrow [\D\rightarrow \D]$ and
$G:[\D\rightarrow \D]\rightarrow \D$. We prove on
one hand that natural intersection type preorders
induces natural $\lambda$-structures, on the other
hand that natural $\lambda$-structures admits
presentations through intersection type
preorders. Moreover we give a concise presentations
of classical $D_\infty$ models of untyped
$\lambda$-calculus through suitable natural
intersection type preorders and prove that filter
models induced by them are isomorphic to
$D_\infty$.}
}
@INPROCEEDINGS{bonecompdezagarr04,
AUTHOR = {Eduardo Bonelli and Adriana Compagnoni and
Mariangiola Dezani-Ciancaglini and Pablo Garralda},
TITLE = {Boxed Ambients with Communication Interfaces},
BOOKTITLE = {MFCS '04},
PAGES = {119--148},
YEAR = 2004,
VOLUME = 3153,
EDITOR = {Fiala, Jir\'{\i}and Koubek, V\'aclav and
Kratochv\'{\i}l Jan},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
EDITOR = {Vijay A. Saraswat},
PDF = {http://www.di.unito.it/~dezani/papers/bcdg.pdf},
DARTREPORT = {yes},
ABSTRACT = {We define {\bf BACI} {\it(Boxed Ambients with
Communication Interfaces)}, an ambient calculus
allowing a liberal communication policy. Each
ambient carries its local view of the topic of
conversation (the type of the information being
exchanged) with parents and children that will
condition where it is allowed to stay or migrate to
and which ambients may be allowed to enter it. The
topic of conversation view of ambients can
dynamically change during migration. {\bf BACI} is
flexible enough to allow different topics of
conversation between an ambient and different
parents, without compromising type-safety: it uses
port names for communication and ambient names for
mobility. Capabilities and co-capabilities exchange
port names and run-time typing information to
control mobility. We show the type-soundness of {\bf
BACI} proving that it satisfies the subject
reduction property. Moreover we study its
behavioural semantics by means of a labelled
transition system.}
}
@INPROCEEDINGS{CDGP04:IFIP04,
AUTHOR = {Mario Coppo and Mariangiola Dezani-Ciancaglini and
Elio Giovannetti and Rosario Pugliese},
TITLE = {Dynamic and Local Typing for Mobile Ambients},
CROSSREF = {TCS2004},
PDF = {http://www.di.unito.it/~dezani/papers/cdgp.pdf},
PAGES = {583--596},
DARTREPORT = {yes},
ABSTRACT = {An ambient calculus with both static and dynamic
types is presented, where the latter ones represent
mobility and access rights that may be dynamically
consumed and acquired in a controlled way. Novel
constructs and operations are provided to this
end. Type-checking is purely local, except for a
global hierarchy that establishes which locations
have the authority to grant rights to which: there
is no global environment (for closed terms)
assigning types to names. Each ambient or process
move is subject to a double authorization, one
static and the other dynamic: static type-checking
controls (communication and) ``active'' mobility
rights, i.e., where a given ambient or process has
the right to go; dynamic type-checking controls
``passive'' rights, i.e., which ambients a given
ambient may be crossed by and which processes it may
receive.}
}
@INCOLLECTION{CCDGP05:CCDGP05,
AUTHOR = {Mario Coppo and Federico Cozzi and Mariangiola Dezani-Ciancaglini and
Elio Giovannetti and Rosario Pugliese},
TITLE = {A Mobility Calculus with Local and Dependent Types},
BOOKTITLE = {Festschrift},
SERIES = {LNCS},
NOTE = {to appear},
DARTREPORT = {yes},
PDF = {http://www.di.unito.it/~coppo/papers/CCDGP05.pdf},
YEAR = {2005},
ABSTRACT = {We introduce an ambient calculus
that combines ambient mobility with process mobility, uses group names
to group ambients with
homologous features, and exploits co-moves and runtime type
checking to implement flexible policies for controlling process
activities. Types rely on group names and, to support dynamicity,
may \emph{depend} on group variables. Policies can dynamically
change also through installation of co-moves. The compliance with
ambient policies can be checked \emph{locally} to the ambients and
requires no global assumptions. We prove that the type assignment
system and the operational semantics of the calculus are `sound',
and we define a sound and complete type inference algorithm which,
when applied to terms whose type decorations only express the
desired policies, computes the minimal type annotations required
for their execution. As an application of our calculus, we
present a couple of examples and linger on the setting up of policies for
controlling the activities of the objects involved.}
}
@ARTICLE{dezahonsmoto2005,
AUTHOR = {Dezani-Ciancaglini, Mariangiola and Honsell, Furio and
Motohama, Yoko},
TITLE = {Compositional characterization of lambda -terms using intersection types},
JOURNAL = {Theoret.\ Comput.\ Sci.},
FJOURNAL = {Theoretical Computer Science},
VOLUME = {340},
NUMBER = {3},
PAGES = {459--495},
YEAR = {2005},
PDF = {http://www.di.unito.it/~dezani/papers/tcsf.pdf},
DARTREPORT = {yes},
ABSTRACT = {We show how to characterise {\em compositionally} a number of {\em
evaluation} properties of $\lambda$-terms using {\em Intersection
Type} assignment systems. In particular, we focus on termination
properties, such as strong normalisation, normalisation, head
normalisation, and weak head normalisation. We
consider also the persistent versions of such notions. By way of
example, we consider also another evaluation property, unrelated
to termination, namely reducibility to a closed term.
Many of these characterisation results are new, to our knowledge, or
else they streamline, strengthen, or generalise earlier results in the
literature.
The completeness parts of the characterisations are proved
uniformly for all the properties, using a {\em set-theoretical} semantics
of intersection types over suitable kinds of {\em stable} sets. This
technique generalises Krivine's and Mitchell's methods for strong
normalisation to other evaluation properties.}
}
@INPROCEEDINGS{Damiani:TLCA-05,
AUTHOR = {F. Damiani},
TITLE = {Rank-2 Intersection and Polymorphic Recursion},
BOOKTITLE = {TLCA'05},
YEAR = {2005},
PUBLISHER = {Springer},
PAGES = {146-161},
SERIES = {LNCS},
VOLUME = {3461},
ABSTRACT = {
Let |- be a rank-2 intersection type system. We say that a
term is |-{\em-simple} (or just {\em simple} when the system
|- is clear from the context) if system |- can prove that
it has a simple type.
In this paper we propose new typing rules and algorithms that are able to type
recursive definitions that are not simple.
At the best of our knowledge, previous algorithms for typing recursive
definitions in presence of intersection types allow only simple
recursive definitions to be typed. The proposed rules are also
able to type interesting examples of {\em polymorphic recursion}
(i.e., recursive definitions rec $\{x=e\}$ where different
occurrences of $x$ in $e$ are used with different types).
Moreover, the underlying techniques do not depend on particulars
of rank-2 intersection, so they can be applied to other type
systems.
},
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/tlca05.html},
PDF = {http://www.di.unito.it/~damiani/papers/tlca05.pdf},
DARTREPORT = {yes},
ITRSPAPER = {yes}
}
@UNPUBLISHED{Damiani:TLCA-05-ExtVer,
TITLE = {Rank-2 Intersection and Polymorphic Recursion (extended version with proofs)},
AUTHOR = {F. Damiani},
YEAR = {2005},
MONTH = JAN,
DOCUMENTURL = {http://www.di.unito.it/~damiani/papers/tlca05.html},
PDF = {http://www.di.unito.it/~damiani/papers/tlca05wA.pdf},
NOTE = {Internal report. Extended version with proofs of~\cite{Damiani:TLCA-05}},
ABSTRACT = {
Let |- be a rank-2 intersection type system. We say that a
term is |-{\em-simple} (or just {\em simple} when the system
|- is clear from the context) if system |- can prove that
it has a simple type.
In this paper we propose new typing rules and algorithms that are able to type
recursive definitions that are not simple.
At the best of our knowledge, previous algorithms for typing recursive
definitions in presence of intersection types allow only simple
recursive definitions to be typed. The proposed rules are also
able to type interesting examples of {\em polymorphic recursion}
(i.e., recursive definitions rec $\{x=e\}$ where different
occurrences of $x$ in $e$ are used with different types).
Moreover, the underlying techniques do not depend on particulars
of rank-2 intersection, so they can be applied to other type
systems.
},
DARTREPORT = {yes},
ITRSPAPER = {yes}
}
@INPROCEEDINGS{Anc+Dam+Dro+Zuc:ftfjp04,
AUTHOR = {D. Ancona and F. Damiani and S. Drossopoulou and
E. Zucca},
TITLE = {Even More Principal Typings for {J}ava-like
Languages},
DISABLEDDOCUMENTURL = {http://www.disi.unige.it/person/AnconaD/Reports.html#AnconaEtAl04c},
PDF = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP04.pdf},
BOOKTITLE = {ECOOP Workshop on Formal Techniques for Java
Programs (FTfJP 2004)},
YEAR = 2004,
MONTH = JUN,
ADDRESS = {Oslo, Norway},
URL = {http://www.cs.ru.nl/~erikpoll/ftfjp/2004.html},
ABSTRACT = {We propose an innovative type system for Java-like
languages which can infer the minimal set of
assumptions guaranteeing type correctness of a class
\texttt{c}, and generate (abstract) bytecode for
\texttt{c}, by inspecting the source code of
\texttt{c} in isolation. We prove the above
properties of our type system by showing that it has
principal typings. As well known, principal typings
support compositional analysis, whereby a collection
of classes can be safely linked together without
further inspection of the classes' code, provided
that each class has been typechecked in isolation
(intra-checking), and that the mutual class
assumptions are satisfied (inter-checking). We also
develop an algorithm for inter-checking, and prove
it correct.},
DARTREPORT = {yes}
}
@INPROCEEDINGS{aherdezadrosyosh05,
AUTHOR = {Mariangiola Dezani-Ciancaglini and Nobuko Yoshida
and Alex Ahern and
Sophia Drossopoulou},
TITLE = {A {D}istributed {O}bject-{O}riented language
with {S}ession
types},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
BOOKTITLE = {TGC 2005},
NOTE = {to appear},
PDF = {http://www.di.unito.it/~dezani/papers/addy.pdf},
ABSTRACT = {In the age of the world-wide web and mobile computing,
programming communication-centric software becomes increasingly
popular. Thus, programmers and program designers get exposed to
new levels of complexity, including composition of communication
behaviors and guarantee of deadlock freedom of their specified
protocols.
This paper proposes the language ${\mathcal {L}}_{doos}$, a simple distributed
object-oriented language augmented by session communication
primitives and types. ${\mathcal {L}}_{doos}$ provides a flexible object-oriented
programming style for structural interaction protocols by
prescribing channel usages within signatures of distributed classes.
We develop a typing system for ${\mathcal {L}}_{doos}$ and prove its soundness with
respect to the operational semantics. We also show that in ${\mathcal {L}}_{doos}$
there will never be a connection error, a communication error,
nor an incorrect completion between server-client
interactions. These results demonstrate that a consistent
integration of object-oriented language features and session types
offers a compositional method to statically check safety of
communication protocols.},
DARTREPORT = {yes},
YEAR = 2005
}
@UNPUBLISHED{dLF05,
TITLE = {Effect system for {BoCa: a Prolog} Implementation},
AUTHOR = {Ugo de'Liguoro and Giuseppe Falzetta},
DARTREPORT = {yes},
PDF = {http://www.di.unito.it/~deligu/papers/dLF05.pdf},
ABSTRACT = {We describe a Prolog implementation of an algorithm deriving types and sets of constraints
for the Effect system of the calculus BoCa \cite{Bar+Bug+Dez+Sas:journvers}, a dialect of MA.
Both type and constraints are inferred given a process term and a context,
declaring the capacities of the free ambient names in the term.
},
YEAR = 2005
}
@UNPUBLISHED{cozz04,
TITLE = {Type inference for local typing of mobile ambients},
AUTHOR = {Federico Cozzi},
DARTREPORT = {yes},
PDF = {http://www.di.unito.it/~dezani/papers/cozzi.pdf},
ABSTRACT = {A type inference algorithm for the local type system for mobile ambients of \cite{CDGP04:IFIP04} is presented.
It is obtained by applying a combination of techniques to the original typing rules, including a constraint handling and simplification procedure, which is mainly based on unification.
The algorithm employs type schemes and therefore is, in a sense, more general than the original system.
The inference algorithm is then implemented in Prolog.},
YEAR = 2004
}
@COMMENT{{PeterM\ollerNeergaard:thesettingofpmn-ask-for-x-symbolisaddedformysaketoavoidmessingupthebibliographywheneditinginemacs.Thesettingofindent-tabs-modeisforeverybodytohelpavoidunnecessarychangesthatcauseCVSconfusion.LocalVariables:pmn-ask-for-x-symbol:0indent-tabs-mode:nilEnd:Consideralsosettingbibtex-filestoconferences.bib.}}
@PROCEEDINGS{COMETA2003,
TITLE = {Proc. Final Workshop Project COMETA},
YEAR = 2003,
BOOKTITLE = {Proc. Final Workshop Project COMETA},
EDITOR = {Furio Honsell and Marina Lenisa and Marino Miculan},
XVOLUME = {?????????},
SERIES = {ENTCS},
ADDRESS = {Udine, Italy},
MONTH = DEC,
PUBLISHER = {Elsevier/Forum}
}
@PROCEEDINGS{ECOOP2002,
KEY = {EC{\relax OOP} '02},
TITLE = {ECOOP'02 - European Conference on Object-Oriented Programming},
BOOKTITLE = {ECOOP'02 - European Conference on Object-Oriented Programming},
YEAR = 2002,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
VOLUME = 2374
}
@PROCEEDINGS{ECOOP2005,
KEY = {EC{\relax OOP} '05},
TITLE = {ECOOP'05 - European Conference on Object-Oriented Programming},
BOOKTITLE = {ECOOP'05 - European Conference on Object-Oriented Programming},
YEAR = 2005,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
NOTE = {To appear}
}
@PROCEEDINGS{ESOP2003,
TITLE = {Programming Languages \& Systems, 12th European Symp.\ Programming},
BOOKTITLE = {Programming Languages \& Systems, 12th European Symp.\ Programming},
KEY = {ES{\relax OP} '03},
YEAR = 2003,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2618,
PUBLISHER = {Springer},
XDATE = {2003-04-07/---11},
XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
XADDRESS = {Warsaw, Poland},
XNOTE = {held as part of ETAPS 2003},
XEDITOR = {Pierpaolo Degano},
ISBN = {3-540-00886-1}
}
@PROCEEDINGS{ESOP2004,
TITLE = {Programming Languages \& Systems, 13th European Symp.\ Programming},
BOOKTITLE = {Programming Languages \& Systems, 13th European Symp.\ Programming},
KEY = {ES{\relax OP} '04},
YEAR = 2004,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2986,
PUBLISHER = {Springer},
XDATE = {2004-03-29/--04-02},
XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
XADDRESS = {Barcelona, Spain},
XNOTE = {held as part of ETAPS 2004},
XEDITOR = {David Schmidt},
ISBN = {3-540-21313-9}
}
@PROCEEDINGS{ESOP2005,
TITLE = {Programming Languages \& Systems, 14th European Symp.\ Programming},
BOOKTITLE = {Programming Languages \& Systems, 14th European Symp.\ Programming},
KEY = {ES{\relax OP} '05},
YEAR = 2005,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 3444,
PUBLISHER = {Springer},
XDATE = {2005-04-04/---08},
XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
XADDRESS = {Edinburgh, Scotland},
XNOTE = {held as part of ETAPS 2005},
XEDITOR = {Mooly Sagiv},
ISBN = {3-540-25435-8},
DOI = {10.1007/b107380}
}
@PROCEEDINGS{FOSSACS2003,
TITLE = {Proc.\ FoSSaCS '03},
YEAR = 2003,
BOOKTITLE = {Proc.\ FoSSaCS '03},
VOLUME = 2620,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer}
}
@PROCEEDINGS{GPCE2004,
TITLE = {Generative Programming and Component Engineering},
BOOKTITLE = {Generative Programming and Component Engineering},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
VOLUME = 3286,
MONTH = OCT,
YEAR = 2004,
XADDRESS = {Vancouver},
EDITOR = {G. Karsai and E. Visser}
}
@PROCEEDINGS{ICALP2002,
TITLE = {Proc.\ 29th Int'l Coll.\ Automata, Languages, and Programming},
BOOKTITLE = {Proc.\ 29th Int'l Coll.\ Automata, Languages, and Programming},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
VOLUME = 2380,
YEAR = 2002,
DATE = {2002-07-08/---13},
XADDRESS = {Malaga, Spain},
ISBN = {3-540-43864-5}
}
@PROCEEDINGS{ICALP2003,
TITLE = {Proc.\ 30th Int'l Coll.\ Automata, Languages, and Programming},
BOOKTITLE = {Proc.\ 30th Int'l Coll.\ Automata, Languages, and Programming},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
VOLUME = 2719,
YEAR = 2003,
DATE = {2003-06-30/--07-04},
XADDRESS = {Eindhoven},
XEDITOR = { J.C.M. Baeten and J.K. Lenstra and J. Parrow and G.J. Woeginger
}
}
@PROCEEDINGS{ICFP2005,
TITLE = {Proc.\ 10th Int'l Conf.\ Functional Programming},
MONTH = SEP,
YEAR = 2005,
KEY = {IC{\relax FP} '05},
BOOKTITLE = {Proc.\ 10th Int'l Conf.\ Functional Programming},
PUBLISHER = {ACM Press},
XADDRESS = {Tallinn, Estonia},
XEDITOR = {Olivier Danvy and Benjamin C. Pierce},
XORGANIZATION = {ACM},
DATE = {2005-09-26/---28},
ISBN = {1-59593-064-7}
}
@PROCEEDINGS{ICTCS2003,
TITLE = {Proc. Italian Conference on Theoretical Computer Science 2003},
BOOKTITLE = {Proc. Italian Conference on Theoretical Computer Science 2003},
XEDITOR = {Blundo and Laneve},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 2841,
MONTH = OCT,
YEAR = 2003,
PUBLISHER = {Springer},
KEY = {IC{\relax TCS} '03}
}
@PROCEEDINGS{ITRS2002,
XEDITOR = {Steffen van Bakel},
TITLE = {Proceedings of the 2nd Workshop on Intersection Types and Related Systems},
BOOKTITLE = {Proceedings of the 2nd Workshop on Intersection Types and Related Systems},
KEY = {IT{\relax RS} '02},
REMARK = {*****FIX THIS ENTRY*****},
EVENTDATE = {2002-07-26},
PUBLICATIONDATE = {2003-02},
YEAR = 2002,
ELSEVIERURL = {http://www.elsevier.nl/locate/entcs/volume70.html},
NOTE = {The ITRS '02 proceedings appears as vol.\ 70, issue 1 of \emph{Elec.\ Notes in Theoret.\ Comp.\ Sci.}, 2003-02},
ISBN = {0-444-51407-4}
}
@PROCEEDINGS{ITRS2004,
TITLE = {Proc.\ 3rd Int'l Workshop Intersection Types \& Related Systems (ITRS 2004)},
BOOKTITLE = {Proc.\ 3rd Int'l Workshop Intersection Types \& Related Systems (ITRS 2004)},
KEY = {IT{\relax RS} '04},
YEAR = 2005,
NOTE = {The ITRS '04 proceedings appears as vol.\ 136
(2005-07-19) of \emph{Elec.\ Notes in Theoret.\
Comp.\ Sci.}},
PROCEEDINGSPAGESINVOLUME = {1--228},
XPUBLISHER = {Elsevier},
XADDRESS = {Turku, Finland},
XEDITOR = {Mario Coppo and Ferruccio Damiani},
EVENTDATE = {2004-07}
}
@PROCEEDINGS{LPAR2003,
TITLE = {Proc.\ 10th Int'l Conf.\
Logic for Programming Artificial Intelligence \&
Reasoning},
YEAR = 2003,
BOOKTITLE = {Proc.\ 10th Int'l Conf.\
Logic for Programming Artificial Intelligence \&
Reasoning},
EDITOR = {Vardi, Moshe and Voronkov, Andrei},
VOLUME = 2850,
SERIES = {LNCS},
PUBLISHER = {Springer},
ADDRESS = {Almaty, Kazakhstan},
MONTH = SEP
}
@PROCEEDINGS{POPL2004,
TITLE = {Conf.\ Rec.\ POPL '04: 31th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
BOOKTITLE = {Conf.\ Rec.\ POPL '04: 31th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
YEAR = 2004,
XORGANIZATION = {ACM},
KEY = {PO{\relax PL} '04},
XPUBLISHER = {ACM Press},
XMONTH = JAN
}
@PROCEEDINGS{POPL2005,
TITLE = {Conf.\ Rec.\ POPL '05: 32nd {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
BOOKTITLE = {Conf.\ Rec.\ POPL '05: 32nd {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
YEAR = 2005,
XORGANIZATION = {ACM},
KEY = {PO{\relax PL} '05},
XADDRESS = {Long Beach, CA, US},
XPUBLISHER = {ACM Press},
XMONTH = JAN,
DATE = {2005-01-12/---14}
}
@PROCEEDINGS{PPDP2002,
TITLE = {Proc.\ 4rd Int'l Conf.\ Principles \& Practice Declarative Programming},
YEAR = 2002,
KEY = {PP{\relax DP} '02},
BOOKTITLE = {Proc.\ 4rd Int'l Conf.\ Principles \& Practice Declarative Programming},
PUBLISHER = {ACM Press},
XADDRESS = {Pittsburgh, PA, US},
XPUBLISHER = {ACM Press}
}
@PROCEEDINGS{PPDP2003,
TITLE = {Proc.\ 5th Int'l Conf.\ Principles \& Practice Declarative Programming},
YEAR = 2003,
KEY = {PP{\relax DP} '03},
BOOKTITLE = {Proc.\ 5th Int'l Conf.\ Principles \& Practice Declarative Programming},
XADDRESS = {Uppsala, SE},
XPUBLISHER = {ACM Press},
ISBN = {1-58113-705-2}
}
@PROCEEDINGS{PPDP2004,
TITLE = {Proc.\ 6th Int'l Conf.\ Principles \& Practice Declarative Programming},
YEAR = 2004,
KEY = {PP{\relax DP} '04},
BOOKTITLE = {Proc.\ 6th Int'l Conf.\ Principles \& Practice Declarative Programming},
XADDRESS = {Verona, IT},
XPUBLISHER = {ACM Press},
ISBN = {1-58113-819-9}
}
@PROCEEDINGS{SAC-2004,
TITLE = {ACM Symposium on Applied Computing SAC 2004},
BOOKTITLE = {ACM Symposium on Applied Computing SAC 2004},
PUBLISHER = {ACM Press},
YEAR = 2004,
KEY = {SAC '04}
}
@PROCEEDINGS{TCS2004,
TITLE = {IFIP TC1 3rd Int'l Conf.\ Theoret.\ Comput.\ Sci.\ (TCS '04)},
BOOKTITLE = {IFIP TC1 3rd Int'l Conf.\ Theoret.\ Comput.\ Sci.\ (TCS '04)},
KEY = {TCS '04},
XEDITOR = {Jean-Jacques Levy and Ernst W. Mayr and John C. Mitchell},
XADDRESS = {Toulouse, France},
XMONTH = AUG # { 23--26},
YEAR = {2004},
ISBN = {1-4020-8140-5},
PUBLISHER = {Kluwer Academic Publishers}
}
@COMMENT{{PeterM\ollerNeergaard:thesettingofpmn-ask-for-x-symbolisaddedformysaketoavoidmessingupthebibliographywheneditinginemacs.Thesettingofindent-tabs-modeisforeverybodytohelpavoidunnecessarychangesthatcauseCVSconfusion.LocalVariables:pmn-ask-for-x-symbol:0indent-tabs-mode:nilEnd:}}
This file has been generated by
bibtex2html 1.43