@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c 'keywords : "semantics"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@inproceedings{Ancona_FTfJP14,
booktitle = {{Formal techniques for Java-like programs (FTfJP14)}},
keywords = {{semantics, types, objects, coinduction}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf},
author = {Ancona, D.},
title = {{How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics}},
pages = {1:1--1:6},
year = {2014},
articleno = {1},
publisher = {ACM},
abstract = {Small-step operational semantics is the most commonly employed formalism for
proving type soundness of statically typed programming languages, because
of its ability to distinguish stuck from non-terminating computations,
as opposed to big-step operational semantics.
Despite this, big-step operational semantics is more abstract, and more
useful for specifying interpreters.
In previous work we have proposed a new proof technique to prove type soundness
of a Java-like language expressed in terms of its big-step operational semantics.
However the presented proof is rather involved, since it
requires showing that the set of proof trees defining the semantic judgment forms a complete metric space
when equipped with a specific distance function.
In this paper we propose a more direct and abstract approach that exploits a standard and general compactness property
of the metric space of values, that allows approximation of the coinductive big-step semantics in terms of the small-step one;
in this way type soundness can be proved by standard mathematical induction.
}
}
@inproceedings{AnconaECOOP12,
author = {Ancona, D.},
title = {Soundness of {O}bject-{O}riented {L}anguages with
{C}oinductive {B}ig-{S}tep {S}emantics},
booktitle = {E{COOP} 2012 - {O}bject-{O}riented {P}rogramming},
editor = {Noble, J.},
volume = {7313},
pages = {459--483},
publisher = {Springer},
abstract = {It is well known that big-step operational semantics
are not suitable for proving soundness of type systems,
because of their inability to distinguish stuck from
non-terminating computations. We show how this problem
can be solved by interpreting coinductively the rules
for the standard big-step operational semantics of a
Java-like language, thus making the claim of soundness
more intuitive: whenever a program is well-typed, its
coinductive operational semantics returns a value.
Indeed, coinduction allows non-terminating computations
to return values; this is proved by showing that the
set of proof trees defining the semantic judgment forms
a complete metric space when equipped with a proper
distance function. In this way, we are able to prove
soundness of a nominal type system w.r.t. the
coinductive semantics. Since the coinductive semantics
is sound w.r.t. the usual small-step operational
semantics, the standard claim of soundness can be
easily deduced. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaECOOP12.pdf},
keywords = {semantics, types, objects, coinduction},
year = 2012
}
@inproceedings{AnconaFTfJP11,
author = {Ancona, D.},
title = {Coinductive big-step operational semantics for type
soundness of {J}ava-like languages},
booktitle = {Formal {T}echniques for {J}ava-like {P}rograms
({FT}f{JP}11)},
pages = {5:1--5:6},
publisher = {ACM},
abstract = {We define a coinductive semantics for a simple
Java-like language by simply interpreting coinductively
the rules of a standard big-step operational semantics.
We prove that such a semantics is sound w.r.t. the
usual small-step operational semantics, and then prove
soundness of a conventional nominal type system w.r.t.
the coinductive semantics. From these two results,
soundness of the type system w.r.t. the small-step
semantics can be easily deduced. This new proposed
approach not only opens up new possibilities for
proving type soundness, but also provides useful
insights on the connection between coinductive big-step
operational semantics and type systems.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP11.pdf},
isbn = {978-1-4503-0893-9},
keywords = {semantics, types, objects, coinduction},
year = 2011
}
@article{AFZ-ENTCS08,
author = {Ancona, D. and Fagorzi, S. and Zucca, E.},
title = {A parametric calculus for mobile open code},
journal = {Electronic Notes in Theoretical Computer Science},
volume = 192,
number = 3,
pages = {3 - 22},
note = {Proceedings of the Third International Workshop on
Developments in Computational Models (DCM 2007)},
abstract = {We present a simple parametric calculus of processes
which exchange open mobile code, that is, code which
may contain free variables to be bound by the
receiver's code. Type safety is ensured by a
combination of static and dynamic checks. That is,
internal consistency of each process is statically
verified, by relying on local type assumptions on
missing code; then, when code is sent from a process to
another, a runtime check based on a subtyping relation
ensures that it can be successfully received, without
requiring re-inspection of the code. In order to refuse
communication in as few cases as possible, the runtime
check accepts even mobile code which would be rejected
if statically available, by automatically inserting
coercions driven by the subtyping relation, as in the
so-called Penn translation. The calculus is parametric
in some ingredients which can vary depending on the
specific language or system. Notably, we abstract away
from the specific nature of the code to be exchanged,
and of the static and dynamic checks. We formalize the
notion of type safety in our general framework and
provide sufficient conditions on the above ingredients
which guarantee this property. We illustrate our
approach on a simple lambda-calculus with records,
where type safe exchange of mobile code is made
problematic by conflicts due to components which were
not explicitly required. In particular, we show that
the standard coercion semantics given in the
literature, with other aims, for this calculus, allows
to detect and eliminate conflicts due to inner
components, thus solving a problem which was left open
in previous work on type-safe exchange of mobile code.},
doi = {DOI: 10.1016/j.entcs.2008.10.024},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ENTCS08.pdf},
keywords = {types, semantics},
url = {http://www.sciencedirect.com/science/article/B75H1-4TVSXYD-2/2/fa909596cba334aeb406667bdfd71e90},
year = 2008
}
@article{AZ-MSCS02,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Mixin Modules: Algebraic Laws and
Reduction Semantics},
journal = {Mathematical Structures in Computer Science},
volume = 12,
number = {6},
pages = {701--737},
abstract = {Mixins are modules which may contain deferred
components, i.e. components not defined in the module
itself; moreover, in contrast to parameterized modules
(like ML functors), they can be mutually dependent and
allow their definitions to be overridden. In a
preceding paper we have defined syntax and denotational
semantics of a kernel language of mixin modules. Here,
we take instead an axiomatic approach, giving a set of
algebraic laws expressing the expected properties of a
small set of primitive operators on mixins.
Interpreting axioms as rewriting rules, we get a
reduction semantics for the language and prove the
existence of normal forms. Moreover, we show that the
model defined in the earlier paper satisfies the given
axiomatization. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/MSCS01.ps.gz},
keywords = {components, semantics},
year = 2002
}
@inproceedings{ACZ-WADT00,
author = {D. Ancona and M. Cerioli and E. Zucca},
title = {Extending {C}asl with Late Binding},
booktitle = {W{ADT}'99 - 14th {W}orkshop on {A}lgebraic
{D}evelopment {T}echniques - {S}elected {P}apers},
editor = {Bert, D. and Choppy, C.},
volume = {1827},
series = {Lecture Notes in Computer Science},
pages = {53--72},
publisher = {Springer Verlag},
abstract = {We define an extension of CASL, the standard language
for algebraic specification, with a late binding
mechanism. More precisely, we introduce a special kind
of functions called methods, for which, differently to
what happens for usual functions, overloading
resolution is delayed at evaluation time and not
required to be conservative. The extension consists, at
the semantic level, in the definition of an institution
LB supporting late binding which is defined on top of
the standard subsorted institution of CASL and, at the
linguistic level, in the enrichment of the CASL
language with appropriate constructs for dealing with
methods.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DISI-TR-99-14.ps.gz},
keywords = {semantics, objects},
year = 2000
}
@inproceedings{Anc-AMAST00,
author = {D. Ancona},
title = {{MIX(FL)}: a kernel language of mixin modules},
booktitle = {A{MAST} 2000 - {A}lgebraic {M}ethodology and
{S}oftware {T}echnology},
editor = {T. Rus},
volume = {1816},
series = {Lecture Notes in Computer Science},
pages = {454--468},
publisher = {Springer Verlag},
abstract = {We define the language of mixin modules MIX(FL) with
the aim of providing foundations for the design of
module systems supporting mixins. Several working
examples are presented showing the benefits of the use
of mixins and overriding in module systems. The
language is strongly typed and supports separate
compilation. The denotational semantics of the language
is based on an algebraic approach and is parametric in
the semantics of the underlying core language. Hence,
even though the language is defined on top of a
specific core language, other kinds of core languages
could be considered as well.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DISI-TR-96-23.ps.gz},
keywords = {components, semantics},
year = 2000
}
@inproceedings{ACZ-FASE99,
author = {D. Ancona and M. Cerioli and E. Zucca},
title = {A formal framework with late binding},
booktitle = {F{ASE}'99 - {F}undamental {A}pproaches to {S}oftware
{E}ngineering},
editor = {Finance, J.-P.},
volume = {1577},
series = {Lecture Notes in Computer Science},
pages = {30--44},
publisher = {Springer Verlag},
abstract = {We define a specification formalism (formally, an
institution) which provides a notion of dynamic type
(the type which is associated to a term by a particular
evaluation) and late binding (the fact that the
function version to be invoked in a function
application depends on the dynamic type of one or more
arguments). Hence, it constitutes a natural formal
framework for modeling object-oriented and other
dynamically-typed languages and a basis for adding to
them a specification level. In this respect, the main
novelty is the capability of writing axioms related to
a given type which are not required to hold for
subtypes, hence can be ``overridden'' in further
refinements, thus lifting at the specification level
the possibility of reusing code which is offered by the
object-oriented approach. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FASE99.ps.gz},
keywords = {semantics, objects},
year = 1999
}
@inproceedings{Anc-WADT99,
author = {D. Ancona},
title = {An Algebraic Framework for Separate Type-Checking},
booktitle = {W{ADT}'98 - 13th {W}orkshop on {A}lgebraic
{D}evelopment {T}echniques - {S}elected {P}apers},
editor = {J. Fiadeiro},
volume = {1589},
series = {Lecture Notes in Computer Science},
pages = {1--15},
publisher = {Springer Verlag},
abstract = {We address the problem of defining an algebraic
framework for modularization supporting separate
type-checking. In order to do that we introduce the
notions of abstract type system and logic of
constraints and we present a canonical construction of
a model part, on top of a logic of constraints. This
canonical construction works under reasonable
assumptions on the underlying type system (e.g.,
soundness of the system). We show that the framework is
suitable for defining the static and dynamic semantics
of module languages, by giving a concrete example of
construction on top of the type system of a simple
typed module language. As a result, the subtyping
relation between module interfaces is captured in a
natural way by the notion of signature morphism. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/WADT98.ps.gz},
keywords = {semantics, types},
year = 1999
}
@article{AZ-MSCS98,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Mixin Modules: Basic and Derived Operators},
journal = {Mathematical Structures in Computer Science},
volume = 8,
number = 4,
pages = {401-446},
abstract = {Mixins are modules in which some components are
deferred, i.e. their definition has to be provided by
another module. Moreover, differently from
parameterized modules (like ML functors), mixin modules
can be mutually dependent and their composition
supports redefinition of components (overriding). In
this paper, we present a formal model of mixins and
their basic composition operators. These operators can
be viewed as a kernel language with clean semantics in
which to express more complex operators of existing
modular languages, including variants of inheritance in
object oriented programming. Our formal model is given
in an "institution independent" way, i.e. is
parameterized by the semantic framework modeling the
underlying core language.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/MSCS98.ps.gz},
keywords = {components, semantics},
month = aug,
year = 1998
}
@techreport{AZ98,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Modules with State},
institution = {Dipartimento di Informatica e Scienze dell'Informazione, Universit\`a di Genova},
number = {DISI-TR-98-10},
abstract = {We propose a new way of handling imperative features
in the algebraic approach to composition of software
modules, meant in its abstract categorical formulation.
The basic idea is to consider, instead of a global
state, orthogonal to the modular structure, the local
state of a module as the collection of those components
which have no associated definition but an extension
which may vary dynamically. Following this intuition,
composition of modules via classical operators like
merge, renaming and hiding involves composition of the
corresponding states, allowing one to give a truly
compositional semantics of module languages. Thanks to
the abstract categorical formulation, we are able to
define a canonical construction of a framework for
modules with state starting from a framework with no
imperative features. This provides the theoretical
basis for designing languages of modules with state in
a way independent of the underlying core language.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DISI-TR-98-10.ps.gz},
keywords = {components, semantics},
year = 1998
}
@phdthesis{Anc98,
author = {D.~Ancona},
title = {Modular Formal Frameworks for Module Systems},
school = {Dipartimento di Informatica, Universit\`a di Pisa},
abstract = {In this thesis we present two formal frameworks for
modeling modular languages. Following a modular
approach, we separate the module and the core level of
a modular language. On the linguistic side, this
corresponds to define a kernel module language
parametric in the underlying core language. On the
semantic side, this corresponds to build a model part
(in the sense of institutions), on top of a standard
module framework. The standard module framework is a
model part, too, satisfying some additional properties
and intended as the formal counterpart of the core
language. The first formal framework we propose deals
with the notion of state, an essential component of
modules in imperative languages. The second one is
concerned with a notion of module, called mixin, which
includes those of generic module and abstract class. In
both cases, we present two canonical constructions
yielding a formal framework where models denote modules
with state and mixins, respectively, and we define a
set of primitive operations over them. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PhDthesis.ps.gz},
keywords = {semantics, components, objects},
number = {TD-1/98},
year = 1998
}
@inproceedings{AZ-WADT98,
author = {D.~Ancona and E.~Zucca},
title = {An Algebra of Mixin Modules},
booktitle = {W{ADT}'97 - 12th {W}orkshop on {A}lgebraic
{D}evelopment {T}echniques - {S}elected {P}apers},
editor = {Parisi-Presicce, F.},
volume = {1376},
series = {Lecture Notes in Computer Science},
pages = {92--106},
publisher = {Springer Verlag},
abstract = {Mixins are modules which may contain deferred
components, i.e. components not defined in the module
itself, and allow definitions to be overridden. We give
an axiomatic definition of a set of operations for
mixin combination, corresponding to a variety of
constructs existing in programming languages (merge,
hiding, overriding, functional composition, ...). In
particular, we show that they can all be expressed in
terms of three primitive operations (namely, sum,
reduct and freeze), which are characterized by a small
set of axioms. We show that the given axiomatization is
sound w.r.t. to a model provided in some preceding
work. Finally, we prove the existence of anormal form
for mixin expressions.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/WADT97.ps.gz},
keywords = {components, semantics},
year = 1998
}
@inproceedings{AZ-PLILP97,
author = {D.~Ancona and E.~Zucca},
title = {Overriding Operators in a Mixin-Based Framework},
booktitle = {P{LILP} '97 - 9th {I}ntl. {S}ymp. on {P}rogramming
{L}anguages, {I}mplementations, {L}ogics, and
{P}rograms},
editor = {H.~Glaser and P.~Hartel and H.~Kuchen},
volume = {1292},
series = {Lecture Notes in Computer Science},
pages = {47--61},
publisher = {Springer Verlag},
abstract = {We show that many different overriding operators
present in programming languages can be expressed,
adopting a mixin-based framework, in terms of three
basic operators. In particular we propose two
orthogonal classifications: strong (the overridden
definition is canceled) or weak (the overridden
definition still remains significant, as in Smalltalk's
super feature), and preferential (priority to one of
the two arguments) or general. We formalize the
relation between all these versions. Our analysis and
results are not bound to a particular language, since
they are formulated within an algebraic framework for
mixin modules which can be instantiated over different
core languages.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PLILP97.ps.gz},
keywords = {semantics, objects, components},
year = 1997
}
@inproceedings{AZ-ALP96,
author = {D.~Ancona and E.~Zucca},
title = {An Algebraic Approach to Mixins and Modularity},
booktitle = {A{LP} '96 - 5th {I}ntl. {C}onf. on {A}lgebraic and
{L}ogic {P}rogramming},
editor = {Hanus, M. and Rodr\'{\i}guez-Artalejo, M.},
volume = {1139},
series = {Lecture Notes in Computer Science},
pages = {179--193},
publisher = {Springer Verlag},
abstract = {We present an algebraic formalization of the notion of
mixin module, i.e. a module where the definition of
some components is deferred. Moreover, we define a set
of basic operators for composing mixin modules,
intended to be a kernel language with clean semantics
in which to express more complex operators of existing
modular languages, including variants of inheritance in
object oriented programming. The semantics of the
operators is given in an institution independent way,
i.e. is parameterized on the semantic framework
modeling features of the underlying core language.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ALP96.ps.gz},
keywords = {semantics, components},
year = 1996
}
@inproceedings{AZ-AMAST96,
author = {D.~Ancona and E.~Zucca},
title = {A Formal Framework for Modules with State},
booktitle = {A{MAST} '96 - {A}lgebraic {M}ethodology and {S}oftware
{T}echnology},
editor = {M. Wirsing and M. Nivat},
volume = {1101},
series = {Lecture Notes in Computer Science},
pages = {148--162},
publisher = {Springer Verlag},
abstract = {We present a module algebra interpreted in the model
of dynamic data-types. A data-type with state, or
dynamic data type, is a data type in which the
interpretation of operation symbols is depending on the
internal state, which may change during the time. We
formalize the above notion by a new mathematical
structure, called object structure. From the point of
view of programming languages, an object structure is
the overall semantic value (the denotation) of a
software module in an imperative context: Ada packages,
Modula-2 modules and objects of object based languages
can be thought as syntactic counterparts of object
structures. Thus a first result of our approach is an
abstract and natural definition of the semantic value
of a whole module. A further result that we want to
achieve is this semantics to be truly compositional,
i.e. operations of composing modules to be interpreted
as operations of object structures at the semantic
level. We illustrate that by giving syntax and
semantics of a module language which is parametric in
the concrete syntax used for defining methods and
components of the state. The introduction of state
makes necessary to review the semantics of classical
operators as given in a standard algebraic setting. In
particular, we introduce a distinction between the
visible and the internal signature of an object
structure, which is essential for defining a reduct
operation, hence for modelling export/hiding operators.
Composition of visible signatures must be propagated to
internal signatures in order to keep unchanged hidden
components modulo renaming; this corresponds to
consider co-products of particular diagrams in the
category of signatures.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/AMAST96.ps.gz},
keywords = {semantics, components},
year = 1996
}
@inproceedings{AAZ-ISCORE93,
author = {D. Ancona and E. Astesiano and E. Zucca},
title = {Towards a Classification of Inheritance Relations},
booktitle = {Proc. {ISCORE} '93 ({I}nternational {W}orkshop on
{I}nformation {S}ystems - {C}orrectness and
{R}eusability)},
editor = {U.W. Lipeck and G. Koschorreck},
number = {01/93},
series = {Informatik-Berichte},
pages = {90--113},
publisher = {Universitaet Hannover},
abstract = {We address the problem of providing a rigorous formal
model for classes of objects and the variety of
inheritance relations. Classes are modelled by a new
structure, called d-oid, which corresponds to see
objects as data with state. The approach we take is a
rather abstract one and so we model representation
independent configurations of an object system by
algebras, object identities by so called tracking map,
and method calls as transformations of algebras. Seeing
classes as d-oids allows us to define a hierarchy of
inheritance relations, modelled by relations between
d-oids and corresponding to different liberty levels in
redefining methods. The classification we present
distinguish essentially three levels of inheritance:
minimal, regular and conservative.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/IWIS93.ps.gz},
keywords = {semantics, objects},
year = 1993
}
This file was generated by bibtex2html 1.98.