This page contains most of my publications ordered according to their topic (the same
publication may appear in different topics). The complete list is here. The same publications ordered by type are in this page.
[ Page automatically generated on Wednesday, 12 May 2021
from the following file(s): /home/beppe/BIBLIO/castagna-unp.bib /home/beppe/BIBLIO/castagna.bib ]
Type theory and subtyping
G. Castagna, M. Laurent, V. Lanvin, and K. Nguyen: Revisiting Occurrence Typing, June, 2019. Unpublished manuscript. [Abstract] We revisit occurrence typing, a technique to refine the type of
variables occurring in type-cases and, thus, capture some programming
patterns used in untyped languages. Although occurrence typing was
tied from its inception to set-theoretic types―union types, in
particular―it never fully exploited the capabilities of these types. Here
we show how, by using set-theoretic types, it is possible to develop a
general typing framemork that encompasses and generalizes several
aspects of current occurrence typing proposals and that can be applied to
tackle other problems such as the inference of intersection types for functions
and the optimization of the compilation of gradually typed languages.[BibTeX] Click for bibtex entry@unpublished{CLLN19,
author = {G. Castagna and M. Laurent and V. Lanvin and K. Nguyen},
title = {Revisiting Occurrence Typing},
note = {Unpublished manuscript},
month = {jun},
year = {2019},
}
G. Castagna: Object-Oriented Programming: A Unified Foundation, Birkäuser, Progress in Theoretical Computer Science Series, 1997. ISBN 3-7643-3905-5 (hardcover, 388 pages). [BibTeX]Click for bibtex entry@book{oobook,
author = {G. Castagna},
title = {Object-Oriented Programming: A Unified Foundation},
publisher = {Birk{ä}user},
year = {1997},
series = {Progress in Theoretical Computer Science Series},
address = {Boston},
note = {ISBN 3-7643-3905-5 (hardcover, 388 pages)},
}
G. Castagna: Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers). Logical Methods in Computer Science, n. 16, pag. 15:1―15:58, 2020. [Abstract] Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language.
In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue.
Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers.
Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.[BibTeX] Click for bibtex entry@article{Cas15,
author = {G. Castagna},
title = {Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers)},
journal = {Logical Methods in Computer Science},
year = {2020},
number = {16},
pages = {15:1--15:58},
note = {\ifFRENCH\else First version: 2013.\fi},
}
Giuseppe Castagna, Mariangola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani: Foundations of Session Types: 10 Years Later. In Principles and Practice of Programming Languages 2019 (PPDP ’19), pag. 1-3, ACM, New York, 2019. Invited talk, Most Influential Paper 10-Years Award. [BibTeX]Click for bibtex entry@inproceedings{CDGP19,
author = {Giuseppe Castagna and Mariangola Dezani-Ciancaglini and Elena Giachino and Luca Padovani},
title = {Foundations of Session Types: 10 Years Later},
booktitle = {Principles and Practice of Programming Languages 2019 (PPDP ’19)},
year = {2019},
pages = {1-3},
publisher = {ACM, New York},
note = {Invited talk, \textit{Most Influential Paper 10-Years Award}},
}
G. Castagna, G. Duboc, V. Lanvin, and J. G. Siek: A space-efficient call-by-value virtual machine for gradual set-theoretic types. In IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages, September, 2019. [Abstract] We describe the design and implementation of a virtual
machine for programming languages that use gradual typing with
set-theoretic types focusing on practical issues such as runtime
space efficiency, and efficient implementation of tail recursive calls.[BibTeX] Click for bibtex entry@inproceedings{CDLS19,
author = {G. Castagna and G. Duboc and V. Lanvin and J. G. Siek},
title = {A space-efficient call-by-value virtual machine for gradual set-theoretic types},
booktitle = {IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages},
year = {2019},
month = {sep},
}
Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca: Semantic subtyping for non-strict languages. In 24th International Conference on Types for Proofs and Programs (TYPES 2018), vol. 130, Leibniz International Proceedings in Informatics (LIPIcs), pag. 4:1―4:24, Schloss Dagstuhl―Leibniz-Zentrum fuer Informatik, 2019. [Abstract] Semantic subtyping is an approach to define subtyping relations
for type systems featuring union and intersection type connectives.
It has been studied only for strict languages,
and it is unsound for non-strict semantics.
In this work, we study how to adapt this approach to non-strict languages:
in particular, we define a type system using semantic subtyping
for a functional language with a call-by-need semantics.
We do so by introducing an explicit representation for divergence in the types,
so that the type system distinguishes expressions that are results
from those which are computations that might diverge.[BibTeX] Click for bibtex entry@inproceedings{types18post,
author = {Tommaso Petrucciani and Giuseppe Castagna and Davide Ancona and Elena Zucca},
title = {Semantic subtyping for non-strict languages},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
year = {2019},
volume = {130},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
pages = {4:1--4:24},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
}
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek: Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, Article 16, n. POPL '19: 46th ACM Symposium on Principles of Programming Languages, January, 2019. [Abstract] We define a new, more semantic interpretation of gradual types and use it to "gradualize" two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism.
In particular, we use the new interpretation to define two preorders on types, subtyping and materialization, and we employ these preorders to define three gradual type systems ―Hindley-Milner, with subtyping, and with union and intersection types― which we present in two different forms: declaratively and algorithmically.
The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the existing standard rules of the type system. This yields clearer, more intelligible, and streamlined definitions; it also shows a direct correlation between cast insertion and materialization that suggests a logical interpretation of the cast calculus, an essential component of gradual typing systems. For the algorithmic presentation, we show how it can be defined by using already existing constraint solving algorithms simply by adding some pre-/post-processing steps. We relate corresponding declarative and algorithmic presentations by soundness and completeness results.
As customary, the semantics of the various gradually-typed languages is given in terms of a compilation into cast calculi that use blame labels to pinpoint cast failures. To that end, we show how to define the operational semantics for casts in the presence of unions and intersections, which is an important and far-from-obvious result. We also show a direct correlation between the safety of a cast and the "polarity" of its blame label, allowing for a simpler formulation of the so-called blame safety property.[BibTeX] Click for bibtex entry@article{CLPS19,
author = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G.~Siek},
title = {Gradual Typing: a New Perspective},
journal = {Proc. ACM Program. Lang.},
year = {2019},
volume = {3, Article 16},
number = {POPL\,'19: 46th ACM Symposium on Principles of Programming Languages},
month = {jan},
}
G. Castagna and V. Lanvin: Gradual Typing with Union and Intersection Types. Proc. ACM
Program. Lang., vol. 1, Article 41, n. ICFP '17, September, 2017. [Abstract] We propose a type system for functional languages with gradual types
and set-theoretic type connectives and prove its soundness. In
particular, we show how to lift the definition of the domain and
result type of an application from non-gradual types to gradual ones
and likewise for the subtyping relation. We also show that deciding
subtyping for gradual types can be reduced in linear time to deciding
subtyping for non-gradual types and that the same holds true for all
subtyping-related decision problems that must be solved for type
inference. More generally, this work not only enriches gradual type
systems with unions and intersections and with the type precision that
arise from their use, but also proposes and advocates a new style of
gradual types programming where union and intersection types are used
by programmers to instruct the system to perform fewer dynamic checks.[BibTeX] Click for bibtex entry@article{CL17,
author = {G. Castagna and V. Lanvin},
title = {Gradual Typing with Union and Intersection Types},
journal = {Proc. ACM
Program. Lang.},
year = {2017},
volume = {1, Article 41},
number = {ICFP\,'17},
month = {sep},
}
D. Ancona, V. Bono, M. Bravetti, G. Castagna, J. Campos, P.-M. Deniélou, S. Gay, N. Gesbert, E. Giachino, R. Hu, E. Broch Johnsen, F. Martins, V. Mascardi, F. Montesi, N. Ng, R. Neykova, L. Padovani, V. Vasconcelos, and N. Yoshida: Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, vol. 3, pag. 95-230, 2016. [BibTeX]Click for bibtex entry@article{soar16,
author = {D. Ancona and V. Bono and M. Bravetti and G. Castagna and J. Campos and P.-M. Deniélou and S. Gay and N. Gesbert and E. Giachino and R. Hu and E. Broch Johnsen and F. Martins and V. Mascardi and F. Montesi and N. Ng and R. Neykova and L. Padovani and V. Vasconcelos and N. Yoshida},
title = {{Behavioral Types in Programming Languages}},
journal = {Foundations and Trends in Programming Languages},
year = {2016},
volume = {3},
pages = {95-230},
}
G. Castagna, T. Petrucciani, and K. Nguyễn: Set-Theoretic Types for Polymorphic Variants. In ICFP '16, 21st ACM SIGPLAN International Conference on Functional Programming, pag. 378-391, September, 2016. [Abstract] Polymorphic variants are a useful feature of the OCaml language whose
current definition and implementation rely on kinding constraints to
simulate a subtyping relation via unification. This yields an awkward
formalization and results in a type system whose behaviour is in some
cases unintuitive and/or unduly restrictive.
In this work, we present an alternative formalization of polymorphic
variants, based on set-theoretic types and subtyping, that yields
a cleaner and more streamlined system. Our formalization is more
expressive than the current one (it types more programs while preserving
type safety), it can internalize some meta-theoretic properties, and it
removes some pathological cases of the current implementation resulting
in a more intuitive and, thus, predictable type system.
More generally, this work shows how to add full-fledged union types to
functional languages of the ML family that usually rely on the
Hindley-Milner type system. As an aside, our system also improves
the theory of semantic subtyping, notably by proving completeness for
the type reconstruction algorithm.[BibTeX] Click for bibtex entry@inproceedings{CPN16,
author = {G. Castagna and T. Petrucciani and K. Nguyễn},
title = {Set-Theoretic Types for Polymorphic Variants},
booktitle = {ICFP\,'16, 21st ACM SIGPLAN International Conference on Functional Programming},
year = {2016},
pages = {378-391},
month = {sep},
}
G. Castagna, H. Im, K. Nguyễn, and V. Benzaken: A Core Calculus for XQuery 3.0. In ESOP '15: 24th European Symposium on Programming, n. 5710, LNCS, pag. 232-256, Springer, 2015. [Abstract] XML processing languages can be classified according to whether they
extract XML data by paths or pattern matching. In the former category
one finds XQuery, in the latter XDuce and CDuce. The
strengths of one category correspond to the weaknesses of the other.
In this work, we propose to bridge the gap between two of these
languages: XQuery and CDuce. We do it by extending CDuce so as it
can be seen as a succinct core lambda-calculus that
captures XQuery 3.0 programs. The extensions we consider essentially
allow CDuce to implement by pattern matching XPath-like navigation
expressions and to precisely type them. The encoding of XQuery 3.0
into the extension of CDuce provides a formal semantics and a sound
static type system for XQuery 3.0 programs.[BibTeX] Click for bibtex entry@inproceedings{CHNB15,
author = {G. Castagna and H. Im and K. Nguyễn and V. Benzaken},
title = {A Core Calculus for {XQuery} 3.0},
booktitle = {ESOP\,'15: 24th European Symposium on Programming},
year = {2015},
number = {5710},
series = {LNCS},
pages = {232-256},
publisher = {Springer},
}
G. Castagna, K. Nguyễn, Z. Xu, and P. Abate: Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. In POPL '15, 42nd ACM Symposium on Principles of Programming Languages, pag. 289―302, January, 2015. [Slides][Abstract] This article is the second part of a two articles series about
a calculus with higher-order polymorphic functions, recursive types
with arrow and product type constructors and set-theoretic type
connectives (union, intersection, and negation).
In the first part, presented in a companion paper, we defined and
studied the syntax, semantics, and evaluation of the explicitly-typed
version of the calculus, in which type instantiation is driven by
explicit instantiation annotations. In this second part we present a
local type inference system that allows the programmer to omit explicit
instantiation annotations, and a type reconstruction system that allows
the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations
and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce2,
author = {G. Castagna and K. Nguyễn and Z. Xu and P. Abate},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 2}: Local Type Inference and Type Reconstruction},
booktitle = {POPL\,'15, 42nd ACM Symposium on Principles of Programming Languages},
year = {2015},
pages = {289--302},
month = {jan},
}
G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, and L. Padovani: Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In POPL '14, 41st ACM Symposium on Principles of Programming Languages, pag. 5―17, January, 2014. [Slides][Abstract] This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation).
In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce1,
author = {G. Castagna and K. Nguyễn and Z. Xu and H. Im and S. Lenglet and L. Padovani},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 1}: Syntax, Semantics, and Evaluation},
booktitle = {POPL\,'14, 41st ACM Symposium on Principles of Programming Languages},
year = {2014},
pages = {5--17},
month = {jan},
}
V. Benzaken, G. Castagna, K. Nguyễn, and J. Siméon: Static and Dynamic Semantics of NoSQL Languages. In POPL '13, 40th ACM Symposium on Principles of Programming Languages, pag. 101―113, 2013. [Abstract] We present a calculus for processing semistructured data that spans
differences of application area among several novel query lan- guages, broadly categorized as “NoSQL”. This calculus lets users
define their own operators, capturing a wider range of data processing capabilities, whilst providing a typing precision so far typical
only of primitive hard-coded operators. The type inference algorithm is based on semantic type checking, resulting in type infor- mation that is both precise, and flexible enough to handle structured
and semistructured data. We illustrate the use of this calculus by
encoding a large fragment of Jaql, including operations and iterators over JSON, embedded SQL expressions, and co-grouping, and
show how the encoding directly yields a typing discipline for Jaql
as it is, namely without the addition of any type definition or type
annotation in the code.[BibTeX] Click for bibtex entry@inproceedings{BCNS13,
author = {V. Benzaken and G. Castagna and K. Nguyễn and J. Siméon},
title = {Static and Dynamic Semantics of {NoSQL} Languages},
booktitle = {POPL\,'13, 40th ACM Symposium on Principles of Programming Languages},
year = {2013},
pages = {101--113},
}[Extended Version]
V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyễn: Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems, vol. 38, n. 1, pag. 4:1―4:45, 2013. [Abstract] XML data projection (or pruning) is a natural
optimization for main memory query engines: given a
query Q over a document D, the subtrees of D that
are not necessary to evaluate Q are pruned, thus
producing a smaller document D ; the query Q is then
executed on D , hence avoiding to allocate and
process nodes that will never be reached by Q. In
this article, we propose a new approach, based on
types, that greatly improves current solutions.
Besides providing comparable or greater precision
and far lesser pruning overhead, our solution
―unlike current approaches― takes into account
backward axes, predicates, and can be applied to
multiple queries rather than just to single ones. A
side contribution is a new type system for XPath
able to handle backward axes. The soundness of our
approach is formally proved. Furthermore, we prove
that the approach is also complete (i.e., yields the
best possible type-driven pruning) for a relevant
class of queries and Schemas. We further validate
our approach using the XMark and XPathMark
benchmarks and show that pruning not only improves
the main memory query engine's performances (as
expected) but also those of state of the art native
XML databases.[BibTeX] Click for bibtex entry@article{BCCN13,
author = {V. Benzaken and G. Castagna and D. Colazzo and K. Nguyễn},
title = {Optimizing {XML} querying using type-based document projection},
journal = {ACM Transactions on Database Systems},
year = {2013},
volume = {38},
number = {1},
pages = {4:1--4:45},
}
G. Castagna, M. Dezani Ciancaglini, and L. Padovani: On Global Types and Multi-Party Sessions. Logical Methods in Computer Science, vol. 8, n. 1:24, pag. 1―45, 2012. [Slides][Abstract] Global types are formal specifications that describe
communication protocols in terms of their global
interactions. We present a new, streamlined language
of global types equipped with a trace-based
semantics and whose features and restrictions are
semantically justified. The multi-party sessions
obtained projecting our global types enjoy a
liveness property in addition to the traditional
progress and are shown to be sound and complete with
respect to the set of traces of the originating
global type. Our notion of completeness is less
demanding than the classical ones, allowing a
multi-party session to leave out redundant traces
from an underspecified global type. In addition to
the technical content, we discuss some limitations
of our language of global types and provide an
extensive comparison with related specification
languages adopted in different communities.[BibTeX] Click for bibtex entry@article{CDP12,
author = {G. Castagna and M. {Dezani Ciancaglini} and L. Padovani},
title = {On Global Types and Multi-Party Sessions},
journal = {Logical Methods in Computer Science},
year = {2012},
volume = {8},
number = {1:24},
pages = {1--45},
note = {\ifFRENCH Version étendue de~\cite{CDP11}\else Extended version of the invited talk given at FMOODS \& FORTE 2011\fi},
}
G. Castagna and Z. Xu: Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, September, 2011. [Slides][Abstract] Working with XML data often yields to practical situations in which the programmer would need to assign parametric polymorphic types to higher-order functions.
However, up to date, there is no satisfactory way to do it. The
indirect purpose of this article is to define a system to remedy this lack. Its actual goal is to study parametric polymorphism for a type system with
recursive, product, union, intersection, negation, and function types
(the first three constructions are sufficient to encode XML types). We first
recall why the definition of such a system was considered hard―when
not impossible―and then present the main ideas at the basis
of our solution. In particular, we introduce the notion of
``convexity'' on which our solution is built up and discuss
its connections with parametricity as defined by
Reynolds to whose study our work sheds new light.[BibTeX] Click for bibtex entry@inproceedings{CX11,
author = {G. Castagna and Z. Xu},
title = {Set-theoretic Foundation of Parametric Polymorphism and Subtyping},
booktitle = {ICFP\,'11: 16th {ACM-SIGPLAN} International Conference on Functional Programming},
year = {2011},
pages = {94-106},
month = {sep},
}[Extended Version]
G. Castagna, M. Dezani Ciancaglini, and L. Padovani: On Global Types and Multi-Party Sessions. In FMOODS & FORTE 2011, joint 13th IFIP International Conference on Formal Methods for Open Object-based
Distributed Systems and 31st IFIP International Conference on
FORmal TEchniques for Networked and Distributed Systems., n. 6722, LNCS, Springer, 2011. Invited talk. [Slides][Abstract] We present a new, streamlined language of global types equipped with
a trace-based semantics and whose features and restrictions are
semantically justified.
The multi-party sessions obtained projecting our global types enjoy
a liveness property in addition to the traditional progress and are
shown to be sound and complete with respect to the set of traces of
the originating global type.
Our notion of completeness is less demanding than the classical
ones, allowing a multi-party session to leave out redundant traces
from an underspecified global type.
In addition to the technical content, we discuss some limitations of
our language of global types and provide an extensive comparison
with related specification languages adopted in different
communities.[BibTeX] Click for bibtex entry@inproceedings{CDP11,
author = {G. Castagna and M. {Dezani Ciancaglini} and L. Padovani},
title = {On Global Types and Multi-Party Sessions},
booktitle = {{FMOODS \& FORTE 2011}, joint 13th {IFIP}
International Conference on Formal Methods for Open Object-based
Distributed Systems and 31st {IFIP} International Conference on
FORmal TEchniques for Networked and Distributed Systems.},
year = {2011},
number = {6722},
series = {LNCS},
publisher = {Springer},
note = {Invited talk},
}[Extended Version]
G. Castagna and L. Padovani: Contracts for Mobile Processes. In CONCUR 2009, 20th. International
Conference on Concurrency Theory, n. 5710, LNCS, pag. 211-228, Springer, 2009. [Slides][Abstract] Theories identifying well-formed systems of processes―those that are
free of communication errors and enjoy strong properties such as
deadlock freedom―are based either on session types, which are
inhabited by channels, or on contracts, which are inhabited by
processes. Current session type theories impose overly restrictive
disciplines while contract theories only work for networks with fixed
topology. Here we fill the gap between the two approaches by defining
a theory of contracts for so-called mobile processes, those whose
communications may include delegations and channel references.[BibTeX] Click for bibtex entry@inproceedings{CP09,
author = {G. Castagna and L. Padovani},
title = {Contracts for Mobile Processes},
booktitle = {{CONCUR} 2009, 20th.\ International
Conference on Concurrency Theory},
year = {2009},
number = {5710},
series = {LNCS},
pages = {211-228},
publisher = {Springer},
}
H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. ACM Transactions on Programming Languages and Systems, vol. 32, n. 1, pag. 1―56, 2009. [Abstract] Despite the extensiveness of recent investigations on static
typing for XML, parametric polymorphism has rarely been treated.
This well-established typing discipline can also be useful in
XML processing in particular for programs involving ``parametric
schemas,'' i.e., schemas parameterized over other schemas (e.g.,
SOAP). The difficulty in treating polymorphism for XML lies in
how to extend the ``semantic'' approach used in the mainstream
(monomorphic) XML type systems. A naive extension would be
``semantic'' quantification over all substitutions for type
variables. However, this approach reduces to an
NEXPTIME-complete problem for which no practical algorithm is
known. In this paper, we propose a different method that
smoothly extends the semantic approach yet is algorithmically
easier. In this, we devise a novel and simple marking technique, where we interpret a polymorphic type as a set of
values with annotations of which subparts are parameterized. We
exploit this interpretation in every ingredient of our
polymorphic type system such as subtyping, inference of type
arguments, and so on. As a result, we achieve a sensible system
that directly represents a usual expected behavior of
polymorphic type systems―``values of abstract types are never
reconstructed''―in a reminiscence of Reynold's parametricity
theory. Also, we obtain a set of practical algorithms for
typechecking by local modifications to existing ones for a
monomorphic system.[BibTeX] Click for bibtex entry@article{HFC09,
author = {H. Hosoya and A. Frisch and G. Castagna},
title = {Parametric Polymorphism for {XML}},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2009},
volume = {32},
number = {1},
pages = {1--56},
}
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems, vol. 31, n. 5, pag. 1―61, 2009. [Abstract] Contracts are behavioral descriptions of Web services. We devise a
theory of contracts that formalizes the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the
filter, which is an explicit coercion preventing some
possible behaviors of services and, in doing so, make services
compatible with different usage scenarios.
%
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatization of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We outline the practical aspects of our theory by
studying two different concrete syntaxes for contracts and applying each of
them to Web services languages. We also explore implementation issues
of filters and discuss the perspectives of future research this work opens.[BibTeX] Click for bibtex entry@article{CGP09,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2009},
volume = {31},
number = {5},
pages = {1--61},
note = {\ifFRENCH \'Etend et supplante~\cite{CGP08}\else Supersedes the article in POPL '08\fi},
}
V. Benzaken, G. Castagna, H. Hosoya, B.C. Pierce, and S. Vansummeren: The Encyclopedia of Database Systems, chapt. ``XML Typechecking'', Springer, 2009. ISBN 978-0-387-35544-3. [BibTeX]Click for bibtex entry@inbook{EDS,
author = {V. Benzaken and G. Castagna and H. Hosoya and B.C. Pierce and S. Vansummeren},
title = {The Encyclopedia of Database Systems},
chapter = {``{XML} Typechecking''},
publisher = {Springer},
year = {2009},
note = {ISBN 978-0-387-35544-3},
}
G. Castagna and K. Nguyễn: Typed Iterators for XML. In ICFP '08: 13th ACM-SIGPLAN International Conference on Functional Programming, pag. 15―26, April, 2008. [Abstract] XML transformations are very sensitive to types: XML types describe
the tags and attributes of XML elements as well as the number, kind,
and order of their sub-elements. Therefore, even very basic
operations such as changing a tag, renaming an attribute, or adding
an element generally imply conspicuous changes from the type of the
input to the type of the output. Such operations are applied on XML
documents by iterators that,
to be useful, need to be typed by some kind of polymorphism that
goes beyond what currently exists. For this reason these iterators
are not programmed but, rather, hard-coded in the language. However,
this approach soon reaches its limits, as the hard-coded iterators
cannot cover fairly standard usage scenarios.
As a solution to this problem we propose a generic language to define iterators
for XML data to be grafted on some host programming
language. We show that our language mostly offers the required
degree of polymorphism, study its formal properties, and show its
expressiveness and practical impact by providing several usage examples and encodings.[BibTeX] Click for bibtex entry@inproceedings{CN08icfp,
author = {G. Castagna and K. Nguyễn},
title = {Typed Iterators for {XML}},
booktitle = {ICFP '08: 13th {ACM-SIGPLAN} International Conference on Functional Programming},
year = {2008},
pages = {15--26},
month = {apr},
}
A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, vol. 55, n. 4, pag. 1―64, 2008. [Slides][Abstract] Subtyping relations are usually defined either syntactically by a
formal system or semantically by an interpretation of types into an
untyped denotational model. This work shows how to define a subtyping
relation semantically in the presence of Boolean connectives,
functional types and dynamic dispatch on types, without the complexity
of denotational models, and how to derive a complete subtyping
algorithm.[BibTeX] Click for bibtex entry@article{FCB08,
author = {A. Frisch and G. Castagna and V. Benzaken},
title = {Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types},
journal = {Journal of the ACM},
year = {2008},
volume = {55},
number = {4},
pages = {1--64},
note = {\ifFRENCH Inclut et \'etend les articles de LICS '02 et ICALP/PPDP '05 \else Extends and supersedes LICS '02 and ICALP/PPDP '05 articles\fi},
}
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. In POPL '08, 35th ACM Symposium on Principles of Programming Languages, pag. 261―272, January, 2008. [Abstract] Contracts are behavioural descriptions of Web services. We devise a
theory of contracts that formalises the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the definition of
filters, which are explicit coercions that prevent some
possible behaviours of services and, in doing so, they make services compatible
with different usage scenarios.
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatisation of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We also outline the possible practical impact of such a
work and the perspectives of future research it opens.[BibTeX] Click for bibtex entry@inproceedings{CGP08,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
booktitle = {POPL~'08, 35th ACM Symposium on Principles of Programming Languages},
year = {2008},
pages = {261--272},
month = {jan},
}[Extended Version]
G. Castagna, R. De Nicola, and D. Varacca: Semantic subtyping for the π-calculus. Theoretical Computer Science, vol. 398, n. 1-3, pag. 217-242, 2008. Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca. [Abstract] Subtyping relations for the π-calculus are usually defined in a
syntactic way, by means of structural rules. We propose a semantic
characterisation of channel types and use it to derive a subtyping
relation.
The type system we consider includes read-only and
write-only channel types, as well as boolean combinations
of types.
A set-theoretic interpretation of types is provided, in
which boolean combinations of types are interpreted
as the corresponding set-theoretic operations. Subtyping is
defined as inclusion of the interpretations. We prove the
decidability of the subtyping relation and sketch the
subtyping algorithm.
In order to fully exploit the type system,
we define a variant of the π-calculus
where communication is subjected to pattern
matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@article{CDV08,
author = {G. Castagna and R. {De Nicola} and D. Varacca},
title = {Semantic subtyping for the $\pi$-calculus},
journal = {Theoretical Computer Science},
year = {2008},
volume = {398},
number = {1-3},
pages = {217-242},
note = {Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca},
}
G. Castagna, M. Dezani-Ciancaglini, and D. Varacca: Encoding ℂDuce into the ℂPi-calculus. In CONCUR 2006, 17th. International
Conference on Concurrency Theory, n. 4137, LNCS, pag. 310-326, Springer, 2006. [Abstract] CDuce is a functional programming language featuring overloaded functions
and a rich type system with recursive types, subtyping, union, negation and
intersection types. The boolean constructors have a set-theoretic behaviour
defined via a semantic interpretation of the types. The Cpi-calculus is an
extension of the pi-calculus that enriches Pierce and Sangiorgi pi-calculus
subtyping with union, intersection, and negation types. It is based on the
same set-theoretic interpretation as CDuce. In this work we present a
type faithful encoding of the CDuce into the Cpi-calculus. This encoding is
a modification of the Milner-Turner encoding of the lambda-calculus with
subtyping into the pi-calculus with subtyping. The main difficulty to
overcome was to find an encoding of the types that respects the subtyping
relation. Besides the technical challenge, this effort is interesting
because it sheds new light on the Milner-Turner encoding and on the
relations between sequential and remote execution of functions/services, in
particular in the presence of type-driven semantics. It also confirms the
validity of the equational laws for union and intersection types in
pi-calculus.[BibTeX] Click for bibtex entry@inproceedings{CDV06,
author = {G. Castagna and M. Dezani-Ciancaglini and D. Varacca},
title = {Encoding \cduce{} into the \cpi-calculus},
booktitle = {{CONCUR} 2006, 17th.\ International
Conference on Concurrency Theory},
year = {2006},
number = {4137},
series = {LNCS},
pages = {310-326},
publisher = {Springer},
}
G. Castagna: Semantic subtyping: challenges, perspectives, and open problems. In ICTCS 2005, Italian Conference on
Theoretical Computer Science, n. 3701, Lecture Notes in Computer Science, pag. 1―20, Springer, 2005. [Slides][Abstract] Semantic subtyping is a relatively new approach to define
subtyping relations where types are interpreted as sets and
union, intersection and negation types have the corresponding
set-theoretic interpretation. In this lecture we outline the
approach, give an aperçu of its expressiveness and
generality by applying it to the λ-calculus with
recursive and product types and to the π-calculus. We then
discuss in detail the new challenges and research perspectives
that the approach brings forth.[BibTeX] Click for bibtex entry@inproceedings{Cas05b,
author = {G. Castagna},
title = {Semantic subtyping: challenges, perspectives, and open problems},
booktitle = {ICTCS 2005, Italian Conference on
Theoretical Computer Science},
year = {2005},
number = {3701},
series = {Lecture Notes in Computer Science},
pages = {1--20},
publisher = {Springer},
}
G. Castagna and A. Frisch: A gentle introduction to semantic subtyping. In Proceedings of PPDP '05, the 7th ACM SIGPLAN
International Symposium on Principles and Practice
of Declarative Programming, pages 198-208, ACM Press (full version)
and ICALP '05, 32nd International Colloquium on
Automata, Languages and Programming, Lecture Notes
in Computer Science n. 3580, pages 30-34,
Springer (summary), July, 2005. Joint ICALP-PPDP keynote talk. [Slides][Abstract] Subtyping relations are usually defined either syntactically
by a formal system or semantically by an interpretation of types
into an untyped denotational model. In this work we show step by
step how to define a subtyping relation semantically in the
presence of functional types and dynamic dispatch on types,
without the complexity of denotational models, and how to derive
a complete subtyping algorithm. It also provides a recipe to add
set-theoretic union, intersection, and negation types to your
favourite language.
The presentation is voluntarily kept informal and discursive and the
technical details are reduced to a minimum since we rather insist on the
motivations, the intuition, and the guidelines to apply the approach.[BibTeX] Click for bibtex entry@inproceedings{CF05,
author = {G. Castagna and A. Frisch},
title = {A gentle introduction to semantic subtyping},
booktitle = {\emph{Proceedings of} PPDP '05, the 7th ACM SIGPLAN
International Symposium on Principles and Practice
of Declarative Programming, \emph{pages 198-208, ACM Press (full version)
and} ICALP '05, 32nd International Colloquium on
Automata, Languages and Programming, \emph{Lecture Notes
in Computer Science n.\ 3580, pages 30-34,
Springer (summary)}},
year = {2005},
address = {Lisboa, Portugal},
month = {jul},
note = {Joint ICALP-PPDP keynote talk},
}
G. Castagna, R. De Nicola, and D. Varacca: Semantic subtyping for the π-calculus. In LICS '05, 20th Annual IEEE Symposium on Logic in
Computer Science, pag. , IEEE Computer Society Press, 2005. [Abstract] Subtyping relations for the π-calculus are usually
defined in a syntactic way, by means of structural rules. We
propose a semantic characterisation of channel types and use it
to derive a subtyping relation.
The type system we consider includes read-only and write-only
channel types, as well as boolean combinations of types. A
set-theoretic interpretation of types is provided, in which
boolean combinations are interpreted as the corresponding
set-theoretic operations. Subtyping is defined as inclusion of
the interpretations. We prove the decidability of the subtyping
relation and sketch the subtyping algorithm.
In order to fully exploit the type system, we define a
variant of the π-calculus where communication is
subjected to pattern matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@inproceedings{CDV05,
author = {G. Castagna and R. De~Nicola and D. Varacca},
title = {Semantic subtyping for the $\pi$-calculus},
booktitle = {LICS '05, 20th Annual IEEE Symposium on Logic in
Computer Science},
year = {2005},
pages = {},
publisher = {IEEE Computer Society Press},
}
H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. In POPL '05, 32nd ACM Symposium on Principles of Programming Languages, pag. 50-62, ACM Press, 2005. [Abstract] Despite the extensiveness of recent investigations on static
typing for XML, parametric polymorphism has rarely been treated.
This well-established typing discipline can also be useful in
XML processing in particular for programs involving ``parametric
schemas,'' i.e., schemas parameterized over other schemas (e.g.,
SOAP). The difficulty in treating polymorphism for XML lies in
how to extend the ``semantic'' approach used in the mainstream
(monomorphic) XML type systems. A naive extension would be
``semantic'' quantification over all substitutions for type
variables. However, this approach reduces to an
NEXPTIME-complete problem for which no practical algorithm is
known. In this paper, we propose a different method that
smoothly extends the semantic approach yet is algorithmically
easier. In this, we devise a novel and simple marking technique, where we interpret a polymorphic type as a set of
values with annotations of which subparts are parameterized. We
exploit this interpretation in every ingredient of our
polymorphic type system such as subtyping, inference of type
arguments, and so on. As a result, we achieve a sensible system
that directly represents a usual expected behavior of
polymorphic type systems―``values of abstract types are never
reconstructed''―in a reminiscence of Reynold's parametricity
theory. Also, we obtain a set of practical algorithms for
typechecking by local modifications to existing ones for a
monomorphic system.[BibTeX] Click for bibtex entry@inproceedings{HFC05,
author = {H. Hosoya and A. Frisch and G. Castagna},
title = {Parametric Polymorphism for {XML}},
booktitle = {POPL~'05, 32nd ACM Symposium on Principles of Programming Languages},
year = {2005},
pages = {50-62},
publisher = {ACM Press},
}
A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping. In LICS '02, 17th Annual IEEE Symposium on Logic in
Computer Science, pag. 137―146, IEEE Computer Society Press, 2002. [Abstract] Usually subtyping relations are defined either syntactically by a
formal system or semantically by an interpretation of types in
an untyped denotational model. In this work we show how to
define a subtyping relation semantically, for a language whose
operational semantics is driven by types; we
consider a rich type algebra, with product, arrow, recursive,
intersection, union and complement types. Our approach is to
``bootstrap'' the subtyping relation through a notion of
set-theoretic model of the type algebra.
The advantages of the semantic approach are manifold. Foremost
we get ``for free'' many properties (e.g., the transitivity of
subtyping) that, with axiomatized subtyping, would require
tedious and error prone proofs. Equally important is that the
semantic approach allows one to derive complete
algorithms for the subtyping relation or the propagation of
types through patterns. As the subtyping relation has a natural
(inasmuch as semantic) interpretation, the type system can give
informative error messages when static type-checking fails.
Last but not least the approach has an immediate impact in the
definition and the implementation of languages
manipulating XML documents, as this was our original
motivation.[BibTeX] Click for bibtex entry@inproceedings{FCB02,
author = {A. Frisch and G. Castagna and V. Benzaken},
title = {Semantic {S}ubtyping},
booktitle = {LICS '02, 17th Annual IEEE Symposium on Logic in
Computer Science},
year = {2002},
pages = {137--146},
publisher = {IEEE Computer Society Press},
}
G. Castagna and G. Chen: Dependent types with subtyping and late-bound overloading. Information and Computation, vol. 168, n. 1, pag. 1-67, 2001. [Abstract] We present a calculus with dependent types, subtyping and
late-bound overloading. Besides its theoretical interest this
work is motivated by several practical needs that range from the
definition of logic encodings, to proof specialization and
reuse, and to object-oriented extension of the SML module
system.
The theoretical study of this calculus is not straightforward.
While confluence is relatively easy to prove, subject reduction
is much harder. We were not able to add overloading to any
existing system with dependent types and subtyping, and prove
subject reduction. This is why we also define here as by-product
a new subtyping system for dependent types that improves
previous systems and enjoys several properties (notably the
transitivity elimination property). The calculus with
overloading is then obtained as a conservative extension of this
new system. Another difficult point is strong normalization,
which is a necessary condition to the decidability of subtyping
and typing relations. The calculus with overloading is not
strongly normalizing. However, we show that a reasonably useful
fragment of the calculus enjoys this property, and that its
strong normalization implies the decidability of its subtyping
and typing relations.
The article is divided into two parts: the first three sections
provide a general overview of the systems and its motivations,
and can be read separately; the remaining sections develop the
formal study.[BibTeX] Click for bibtex entry@article{CC99,
author = {G. Castagna and G. Chen},
title = {Dependent types with subtyping and late-bound overloading},
journal = {Information and Computation},
year = {2001},
volume = {168},
number = {1},
pages = {1-67},
}
G. Castagna, G. Ghelli, and F. Zappa Nardelli: Typing Mobility in the Seal Calculus. In CONCUR 2001, 12th. International
Conference on Concurrency Theory, n. 2154, LNCS, pag. 82-101, Springer, 2001. [Abstract] The issue of this work is how to type mobility, in the sense
that we tackle the problem of typing not only mobile agents but
also their movement. This yields higher-order types for agents.
To that end we first provide a new definition of the Seal
Calculus that gets rid of existing inessential features while
preserving the distinctive characteristics of the Seal
model. Then we discuss the use of interfaces to type agents and
define the type system. The interpretation induced by this type
system is that interfaces describe interaction effects rather than, as it is customary, provided services. We
discuss at length the difference of the two interpretations and
justify our choice of the former.[BibTeX] Click for bibtex entry@inproceedings{CGZ01,
author = {G. Castagna and G. Ghelli and F. {Zappa Nardelli}},
title = {Typing Mobility in the {S}eal {C}alculus},
booktitle = {{CONCUR} 2001, 12th.\ International
Conference on Concurrency Theory},
year = {2001},
number = {2154},
series = {LNCS},
pages = {82-101},
address = {Aahrus, Danemark},
publisher = {Springer},
}
G. Castagna: Unifying overloading and λ-abstractions: λ^{{}}. Theoretical Computer Science, vol. 176, n. 1-2, pag. 337-345, April, 1997. [Abstract] In this short note we present a minimal system to deal with
overloaded functions with late binding, in which
λ-abstractions are seen as a special case of overloaded
functions with just one code. We prove some relevant properties
that this system enjoys, and show its connection with the
λ&-calculus. We end by showing the practical interest of this
system, in particular in modeling object-oriented languages.[BibTeX] Click for bibtex entry@article{Cas96tcs,
author = {G. Castagna},
title = {Unifying overloading and $\lambda$-abstractions: $\lambda^{\{\}}$},
journal = {Theoretical Computer Science},
year = {1997},
volume = {176},
number = {1-2},
pages = {337-345},
month = {apr},
}
G. Castagna and L. Liquori: A typed calculus of objects. In ASIAN '96, 1st Asian Computing Science Conference, n. 1179, LNCS, pag. 129-141, Springer, 1996. [Abstract] In this paper, we present an explicitly typed version of
the Lambda Calculus of Objects of Fisher, Honsell and Mitchell,
which is a development of the object-calculi defined by Bruce
and Longo. This calculus supports object extension in
presence of object subsumption. Extension is the ability
of modify the behavior of an object by adding new methods (and
inheriting the existing ones). Object subsumption allows to use
objects with a bigger interface in a context expecting another
object with a smaller interface. This calculus has a sound and
decidable type system, ``width'' subtyping, and it allows for
first-class method bodies.[BibTeX] Click for bibtex entry@inproceedings{LC96,
author = {G. Castagna and L. Liquori},
title = {A typed calculus of objects},
booktitle = {ASIAN '96, 1st Asian Computing Science Conference},
year = {1996},
editor = {J.~Jaffar and R.~Yap},
number = {1179},
series = {LNCS},
pages = {129-141},
publisher = {Springer},
}
M.-V. Aponte and G. Castagna: Programmation modulaire avec surcharge et liaison tardive. In Journées Francophones des Langages Applicatifs, 1996. [Abstract] One of the criticisms moved to the SML module system is that it does not
allow code reusing and, more generally, and incremental style of
programming. In this work we propose to extend this module system by adding
overloading and late binding, and we show how by this extension it is
possible to program modules in an incremental style, similar to the one of
object-oriented languages.[BibTeX] Click for bibtex entry@inproceedings{AC96,
author = {M.-V. Aponte and G. Castagna},
title = {Programmation modulaire avec surcharge et liaison tardive},
booktitle = {Journ{é}es Francophones des Langages Applicatifs},
year = {1996},
address = {Val Morin, Qu{é}bec, Canada},
}
G. Castagna: Integration of parametric and ``ad hoc'' second order polymorphism in a calculus with subtyping. Formal Aspects of Computing, vol. 8, n. 3, pag. 247-293, 1996. [Abstract] In this paper we define an extension of F_{≤} to which
we add functions that dispatch on different terms according to the
type they receive as argument. In other words, we enrich the
explicit parametric polymorphism of F_{≤} by an explicit ``ad
hoc'' polymorphism (according the classification of Strachey). We
prove that the calculus we obtain, called F^{&}_{≤}, enjoys the
properties of Church-Rosser and Subject Reduction and that its proof
system is coherent. We also define a significant subcalculus for
which the subtyping is decidable.
This extension has not only a logical interest but it is strongly
motivated by the foundation of a broadly used programming style:
object-oriented programming. The connections between F^{&}_{≤} and
object-oriented languages are widely stressed, and the modeling by
F^{&}_{≤} of some features of the object-oriented style is described,
continuing the work on λ&.[BibTeX] Click for bibtex entry@article{Cas93b,
author = {G. Castagna},
title = {Integration of parametric and ``ad hoc'' second order polymorphism in a calculus with subtyping},
journal = {Formal Aspects of Computing},
year = {1996},
volume = {8},
number = {3},
pages = {247-293},
}
G. Castagna: Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, vol. 17, n. 3, pag. 431-447, 1995. [Abstract] In type-theoretic research on object-oriented programming, the
issue of ``covariance versus contravariance'' is a topic of continuing
debate. In this short note we argue that covariance and
contravariance appropriately characterize two distinct and independent
mechanisms. The so-called contravariance rule correctly captures the
subtyping relation (that relation which establishes which sets
of functions can replace another given set in every context).
A covariant relation, instead, characterizes the specialization of code (i.e., the definition of new code which
replaces old definitions in some particular cases).
Therefore, covariance and contravariance are not opposing views, but
distinct concepts that each have their place in object-oriented
systems. Both can (and should) be integrated in a type-safe manner in
object-oriented languages.
We also show that the independence of the two mechanisms is not
characteristic of a particular model but is valid in general, since
covariant specialization is present in record-based models, although
it is hidden by a deficiency of all existing calculi that realize this
model.
As an aside, we show that the λ&-calculus can be taken
as the basic calculus for both an overloading-based and a record-based
model. Using this approach, one not only obtains a more uniform vision
of object-oriented type theories, but in the case of the record-based
approach, one also gains multiple dispatching, a feature that existing
record-based models do not capture.[BibTeX] Click for bibtex entry@article{Cas94,
author = {G. Castagna},
title = {Covariance and contravariance: conflict without a cause},
journal = {ACM Transactions on Programming Languages and Systems},
year = {1995},
volume = {17},
number = {3},
pages = {431-447},
}
G. Castagna, G. Ghelli, and G. Longo: A calculus for overloaded functions with subtyping. Information and Computation, vol. 117, n. 1, pag. 115-135, February, 1995. [Abstract] We present a simple extension of typed λ-calculus
where functions can be overloaded by putting different
``branches of code'' together. When the function is applied,
the branch to execute is chosen according to a particular
selection rule which depends on the type of the argument. The
crucial feature of the present approach is that the branch
selection depends on the ``run-time type'' of the argument,
which may differ from its compile-time type, because of the
existence of a subtyping relation among types. Hence overloading
cannot be eliminated by a static analysis of code, but is an
essential feature to be dealt with during computation. We obtain
in this way a type-dependent calculus, which differs from the
various λ-calculi where types do not play any role
during computation. We prove Confluence and a generalized
Subject-Reduction theorem for this calculus. We prove Strong
Normalization for a ``stratified'' subcalculus. The definition
of this calculus is guided by the understanding of
object-oriented features and the connections between our
calculus and object-orientedness are extensively stressed. We
show that this calculus provides a foundation for typed
object-oriented languages which solves some of the problems of
the standard record-based approach.[BibTeX] Click for bibtex entry@article{CGL94,
author = {G. Castagna and G. Ghelli and G. Longo},
title = {A calculus for overloaded functions with subtyping},
journal = {Information and Computation},
year = {1995},
volume = {117},
number = {1},
pages = {115-135},
month = {feb},
}
G. Castagna and B.C. Pierce: Decidable Bounded Quantification. In POPL '94, 21st ACM Symposium on Principles of Programming Languages, pag. 151-162, ACM Press, January, 1994. [Abstract] The standard formulation of bounded quantification, system F_{≤}, is
difficult to work with and lacks important syntactic properties, such
as decidability. More tractable variants have been studied, but those
studied so far either exclude significant classes of useful programs
or lack a compelling semantics.
We propose here a simple variant of F_{≤} that ameliorates these
difficulties. It has a natural semantic interpretation, enjoys a
number of important properties that fail in F_{≤}, and includes all
of the programming examples for which F_{≤} has been used in
practice.[BibTeX] Click for bibtex entry@inproceedings{CP93,
author = {G. Castagna and B.C. Pierce},
title = {Decidable Bounded Quantification},
booktitle = {POPL '94, 21st ACM Symposium on Principles of Programming Languages},
year = {1994},
pages = {151-162},
address = {Portland, Oregon},
month = {jan},
publisher = {ACM Press},
}
G. Castagna: F_{≤}^{&} : integrating parametric and ``ad hoc'' second order polymorphism. In DBPL 4, 4th International Workshop on Database Programming Languages, Workshops in Computing, pag. 335-355, Springer, Sep, 1993. Contained in [Cas93b]. [Abstract] In the last years several object-oriented database systems
have come to life. However among them there is a lack of
statically strongly typed languages. This is a very important
deficiency especially for languages, as the database programming
languages, which are designed for complex applications of large
size and that evolve in time.
The absence of such a type discipline is justified by the
complexity of the problem and of the structures it has to be
applied to. Therefore we think that only a fundamental study,
which were able to capture the essential features of the system,
would lead to a typeful object-oriented programming. Thus we
define an extension of F_{≤} to which we add
functions that dispatch on different terms according to the type
they receive as argument. In other words, we enrich the
explicit parametric polymorphism of F_{≤} by an explicit
``ad hoc'' polymorphism (according to the classification
of [Str67]). We prove that the calculus we obtain, called
F^{&}_{≤}, enjoys the properties of Church-Rosser and Subject
Reduction.
This extension constitutes our paradigmatic language for the
foundation of object-oriented programming: the connections
between F^{&}_{≤} and object-oriented languages are widely
stressed, and the modeling by F^{&}_{≤} of some features
of the object-oriented style is described.[BibTeX] Click for bibtex entry@inproceedings{Cas93bea,
author = {G. Castagna},
title = {${F}_{\leq}^{\&}$ : integrating parametric and ``ad hoc'' second order polymorphism},
booktitle = {DBPL 4, 4th International Workshop on Database Programming Languages},
year = {1993},
editor = {C. Beeri and A. Ohori and D. Shasha},
series = {Workshops in Computing},
pages = {335-355},
address = {New York City},
month = {Sep},
publisher = {Springer},
note = {Contained in~\cite{Cas93b}},
}
G. Castagna, G. Ghelli, and G. Longo: A calculus for overloaded functions with subtyping. In ACM Conference on LISP and Functional Programming, pag. 182-192, ACM Press, July, 1992. Extended abstract of [CGL94]. [Abstract] We present a simple extension of typed λ-calculus
where functions can be overloaded by adding different
``pieces of code''. In short, the code of an overloaded function
is formed by several branches of code; the branch to execute is
chosen, when the function is applied, according to a particular
selection rule which depends on the type of the argument. The
crucial feature of the present approach is that a subtyping
relation is defined among types, such that the type of a term
generally decreases during computation, and this fact induces a
distinction between the ``compile-time'' type and the
``run-time'' type of a term. We study the case of overloaded
functions where the branch selection depends on the run-time
type of the argument, so that overloading cannot be eliminated
by a static analysis of code, but is an essential feature to be
dealt with during computation. We obtain in this way a
type-dependent calculus, which differs from the various
λ-calculi where types do not play, essentially, any
rôle during computation. We prove Confluence and Strong
Normalization for this calculus as well as a generalized
Subject-Reduction theorem.
The definition of this calculus is driven by the understanding
of object-oriented features and the connections between our
calculus and object-orientedness are extensively stressed. We
show that this calculus provides a foundation for typed
object-oriented languages which solves some of the problems of
the standard record-based approach. It also provides a
type-discipline for a relevant fragment of the ``core
framework'' of CLOS.[BibTeX] Click for bibtex entry@conference{CGL92,
author = {G. Castagna and G. Ghelli and G. Longo},
title = {A calculus for overloaded functions with subtyping},
booktitle = {ACM Conference on LISP and Functional Programming},
year = {1992},
pages = {182-192},
address = {San Francisco},
month = {jul},
publisher = {ACM Press},
note = {Extended abstract of~\cite{CGL94}},
}
Concurrency theory
Giuseppe Castagna, Mariangola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani: Foundations of Session Types: 10 Years Later. In Principles and Practice of Programming Languages 2019 (PPDP ’19), pag. 1-3, ACM, New York, 2019. Invited talk, Most Influential Paper 10-Years Award. [BibTeX]Click for bibtex entry@inproceedings{CDGP19,
author = {Giuseppe Castagna and Mariangola Dezani-Ciancaglini and Elena Giachino and Luca Padovani},
title = {Foundations of Session Types: 10 Years Later},
booktitle = {Principles and Practice of Programming Languages 2019 (PPDP ’19)},
year = {2019},
pages = {1-3},
publisher = {ACM, New York},
note = {Invited talk, \textit{Most Influential Paper 10-Years Award}},
}
D. Ancona, V. Bono, M. Bravetti, G. Castagna, J. Campos, P.-M. Deniélou, S. Gay, N. Gesbert, E. Giachino, R. Hu, E. Broch Johnsen, F. Martins, V. Mascardi, F. Montesi, N. Ng, R. Neykova, L. Padovani, V. Vasconcelos, and N. Yoshida: Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, vol. 3, pag. 95-230, 2016. [BibTeX]Click for bibtex entry@article{soar16,
author = {D. Ancona and V. Bono and M. Bravetti and G. Castagna and J. Campos and P.-M. Deniélou and S. Gay and N. Gesbert and E. Giachino and R. Hu and E. Broch Johnsen and F. Martins and V. Mascardi and F. Montesi and N. Ng and R. Neykova and L. Padovani and V. Vasconcelos and N. Yoshida},
title = {{Behavioral Types in Programming Languages}},
journal = {Foundations and Trends in Programming Languages},
year = {2016},
volume = {3},
pages = {95-230},
}
G. Castagna, M. Dezani Ciancaglini, and L. Padovani: On Global Types and Multi-Party Sessions. Logical Methods in Computer Science, vol. 8, n. 1:24, pag. 1―45, 2012. [Slides][Abstract] Global types are formal specifications that describe
communication protocols in terms of their global
interactions. We present a new, streamlined language
of global types equipped with a trace-based
semantics and whose features and restrictions are
semantically justified. The multi-party sessions
obtained projecting our global types enjoy a
liveness property in addition to the traditional
progress and are shown to be sound and complete with
respect to the set of traces of the originating
global type. Our notion of completeness is less
demanding than the classical ones, allowing a
multi-party session to leave out redundant traces
from an underspecified global type. In addition to
the technical content, we discuss some limitations
of our language of global types and provide an
extensive comparison with related specification
languages adopted in different communities.[BibTeX] Click for bibtex entry@article{CDP12,
author = {G. Castagna and M. {Dezani Ciancaglini} and L. Padovani},
title = {On Global Types and Multi-Party Sessions},
journal = {Logical Methods in Computer Science},
year = {2012},
volume = {8},
number = {1:24},
pages = {1--45},
note = {\ifFRENCH Version étendue de~\cite{CDP11}\else Extended version of the invited talk given at FMOODS \& FORTE 2011\fi},
}
G. Castagna, M. Dezani Ciancaglini, and L. Padovani: On Global Types and Multi-Party Sessions. In FMOODS & FORTE 2011, joint 13th IFIP International Conference on Formal Methods for Open Object-based
Distributed Systems and 31st IFIP International Conference on
FORmal TEchniques for Networked and Distributed Systems., n. 6722, LNCS, Springer, 2011. Invited talk. [Slides][Abstract] We present a new, streamlined language of global types equipped with
a trace-based semantics and whose features and restrictions are
semantically justified.
The multi-party sessions obtained projecting our global types enjoy
a liveness property in addition to the traditional progress and are
shown to be sound and complete with respect to the set of traces of
the originating global type.
Our notion of completeness is less demanding than the classical
ones, allowing a multi-party session to leave out redundant traces
from an underspecified global type.
In addition to the technical content, we discuss some limitations of
our language of global types and provide an extensive comparison
with related specification languages adopted in different
communities.[BibTeX] Click for bibtex entry@inproceedings{CDP11,
author = {G. Castagna and M. {Dezani Ciancaglini} and L. Padovani},
title = {On Global Types and Multi-Party Sessions},
booktitle = {{FMOODS \& FORTE 2011}, joint 13th {IFIP}
International Conference on Formal Methods for Open Object-based
Distributed Systems and 31st {IFIP} International Conference on
FORmal TEchniques for Networked and Distributed Systems.},
year = {2011},
number = {6722},
series = {LNCS},
publisher = {Springer},
note = {Invited talk},
}[Extended Version]
G. Castagna and L. Padovani: Contracts for Mobile Processes. In CONCUR 2009, 20th. International
Conference on Concurrency Theory, n. 5710, LNCS, pag. 211-228, Springer, 2009. [Slides][Abstract] Theories identifying well-formed systems of processes―those that are
free of communication errors and enjoy strong properties such as
deadlock freedom―are based either on session types, which are
inhabited by channels, or on contracts, which are inhabited by
processes. Current session type theories impose overly restrictive
disciplines while contract theories only work for networks with fixed
topology. Here we fill the gap between the two approaches by defining
a theory of contracts for so-called mobile processes, those whose
communications may include delegations and channel references.[BibTeX] Click for bibtex entry@inproceedings{CP09,
author = {G. Castagna and L. Padovani},
title = {Contracts for Mobile Processes},
booktitle = {{CONCUR} 2009, 20th.\ International
Conference on Concurrency Theory},
year = {2009},
number = {5710},
series = {LNCS},
pages = {211-228},
publisher = {Springer},
}
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems, vol. 31, n. 5, pag. 1―61, 2009. [Abstract] Contracts are behavioral descriptions of Web services. We devise a
theory of contracts that formalizes the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the
filter, which is an explicit coercion preventing some
possible behaviors of services and, in doing so, make services
compatible with different usage scenarios.
%
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatization of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We outline the practical aspects of our theory by
studying two different concrete syntaxes for contracts and applying each of
them to Web services languages. We also explore implementation issues
of filters and discuss the perspectives of future research this work opens.[BibTeX] Click for bibtex entry@article{CGP09,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2009},
volume = {31},
number = {5},
pages = {1--61},
note = {\ifFRENCH \'Etend et supplante~\cite{CGP08}\else Supersedes the article in POPL '08\fi},
}
G. Castagna, M. Dezani-Ciancaglini, E. Giachino, and L. Padovani: Foundations of Session Types. In PPDP '09: 11th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming, pag. 219-230, ACM, 2009. [Abstract] We present a streamlined theory of session types based on a simple
yet general and expressive formalism whose main features are
semantically characterized and where each design choice is semantically
justified. We formally define the semantics of session types and
use it to define the subsessioning relation. We give a coinductive
characterization of subsessioning and describe algorithms to decide
all the key relations defined in the article. We show that all monomorphic
dyadic session types proposed in the literature are particular cases of our session types.[BibTeX] Click for bibtex entry@inproceedings{CDGP09,
author = {G. Castagna and M. Dezani-Ciancaglini and E. Giachino and L. Padovani},
title = {Foundations of Session Types},
booktitle = {PPDP\,'09: 11th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming},
year = {2009},
pages = {219-230},
publisher = {ACM},
}[Extended Version]
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. In POPL '08, 35th ACM Symposium on Principles of Programming Languages, pag. 261―272, January, 2008. [Abstract] Contracts are behavioural descriptions of Web services. We devise a
theory of contracts that formalises the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the definition of
filters, which are explicit coercions that prevent some
possible behaviours of services and, in doing so, they make services compatible
with different usage scenarios.
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatisation of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We also outline the possible practical impact of such a
work and the perspectives of future research it opens.[BibTeX] Click for bibtex entry@inproceedings{CGP08,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
booktitle = {POPL~'08, 35th ACM Symposium on Principles of Programming Languages},
year = {2008},
pages = {261--272},
month = {jan},
}[Extended Version]
G. Castagna, R. De Nicola, and D. Varacca: Semantic subtyping for the π-calculus. Theoretical Computer Science, vol. 398, n. 1-3, pag. 217-242, 2008. Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca. [Abstract] Subtyping relations for the π-calculus are usually defined in a
syntactic way, by means of structural rules. We propose a semantic
characterisation of channel types and use it to derive a subtyping
relation.
The type system we consider includes read-only and
write-only channel types, as well as boolean combinations
of types.
A set-theoretic interpretation of types is provided, in
which boolean combinations of types are interpreted
as the corresponding set-theoretic operations. Subtyping is
defined as inclusion of the interpretations. We prove the
decidability of the subtyping relation and sketch the
subtyping algorithm.
In order to fully exploit the type system,
we define a variant of the π-calculus
where communication is subjected to pattern
matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@article{CDV08,
author = {G. Castagna and R. {De Nicola} and D. Varacca},
title = {Semantic subtyping for the $\pi$-calculus},
journal = {Theoretical Computer Science},
year = {2008},
volume = {398},
number = {1-3},
pages = {217-242},
note = {Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca},
}
A. Phillips, L. Cardelli, and G. Castagna: A Graphical Representation for Biological Processes in the Stochastic pi-calculus. Transactions on Computational Systems Biology, vol. 7, pag. 123-152, 2006. [Abstract] This paper presents a graphical representation for the stochastic
pi-calculus, which is formalised by defining a corresponding graphical
calculus. The graphical calculus is shown to be reduction equivalent to
stochastic pi, ensuring that the two calculi have the same expressive
power. The graphical representation is used to model a couple of example
biological systems, namely a bistable gene network and a mapk signalling
cascade. One of the main benefits of the representation is its ability to
highlight the existence of cycles, which are a key feature of many biological
systems. Another benefit is its ability to animate interactions between
system components, in order to visualise system dynamics. The graphical
representation can also be used as a front end to a simulator for the
stochastic pi-calculus, with a view to making modelling and simulation of
biological systems more accessible to non computer scientists.[BibTeX] Click for bibtex entry@article{PCC06,
author = {A. Phillips and L. Cardelli and G. Castagna},
title = {A Graphical Representation for Biological Processes in the Stochastic pi-calculus},
journal = {Transactions on Computational Systems Biology},
year = {2006},
volume = {7},
pages = {123-152},
}
G. Castagna, M. Dezani-Ciancaglini, and D. Varacca: Encoding ℂDuce into the ℂPi-calculus. In CONCUR 2006, 17th. International
Conference on Concurrency Theory, n. 4137, LNCS, pag. 310-326, Springer, 2006. [Abstract] CDuce is a functional programming language featuring overloaded functions
and a rich type system with recursive types, subtyping, union, negation and
intersection types. The boolean constructors have a set-theoretic behaviour
defined via a semantic interpretation of the types. The Cpi-calculus is an
extension of the pi-calculus that enriches Pierce and Sangiorgi pi-calculus
subtyping with union, intersection, and negation types. It is based on the
same set-theoretic interpretation as CDuce. In this work we present a
type faithful encoding of the CDuce into the Cpi-calculus. This encoding is
a modification of the Milner-Turner encoding of the lambda-calculus with
subtyping into the pi-calculus with subtyping. The main difficulty to
overcome was to find an encoding of the types that respects the subtyping
relation. Besides the technical challenge, this effort is interesting
because it sheds new light on the Milner-Turner encoding and on the
relations between sequential and remote execution of functions/services, in
particular in the presence of type-driven semantics. It also confirms the
validity of the equational laws for union and intersection types in
pi-calculus.[BibTeX] Click for bibtex entry@inproceedings{CDV06,
author = {G. Castagna and M. Dezani-Ciancaglini and D. Varacca},
title = {Encoding \cduce{} into the \cpi-calculus},
booktitle = {{CONCUR} 2006, 17th.\ International
Conference on Concurrency Theory},
year = {2006},
number = {4137},
series = {LNCS},
pages = {310-326},
publisher = {Springer},
}
G. Castagna: Semantic subtyping: challenges, perspectives, and open problems. In ICTCS 2005, Italian Conference on
Theoretical Computer Science, n. 3701, Lecture Notes in Computer Science, pag. 1―20, Springer, 2005. [Slides][Abstract] Semantic subtyping is a relatively new approach to define
subtyping relations where types are interpreted as sets and
union, intersection and negation types have the corresponding
set-theoretic interpretation. In this lecture we outline the
approach, give an aperçu of its expressiveness and
generality by applying it to the λ-calculus with
recursive and product types and to the π-calculus. We then
discuss in detail the new challenges and research perspectives
that the approach brings forth.[BibTeX] Click for bibtex entry@inproceedings{Cas05b,
author = {G. Castagna},
title = {Semantic subtyping: challenges, perspectives, and open problems},
booktitle = {ICTCS 2005, Italian Conference on
Theoretical Computer Science},
year = {2005},
number = {3701},
series = {Lecture Notes in Computer Science},
pages = {1--20},
publisher = {Springer},
}
G. Castagna, R. De Nicola, and D. Varacca: Semantic subtyping for the π-calculus. In LICS '05, 20th Annual IEEE Symposium on Logic in
Computer Science, pag. , IEEE Computer Society Press, 2005. [Abstract] Subtyping relations for the π-calculus are usually
defined in a syntactic way, by means of structural rules. We
propose a semantic characterisation of channel types and use it
to derive a subtyping relation.
The type system we consider includes read-only and write-only
channel types, as well as boolean combinations of types. A
set-theoretic interpretation of types is provided, in which
boolean combinations are interpreted as the corresponding
set-theoretic operations. Subtyping is defined as inclusion of
the interpretations. We prove the decidability of the subtyping
relation and sketch the subtyping algorithm.
In order to fully exploit the type system, we define a
variant of the π-calculus where communication is
subjected to pattern matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@inproceedings{CDV05,
author = {G. Castagna and R. De~Nicola and D. Varacca},
title = {Semantic subtyping for the $\pi$-calculus},
booktitle = {LICS '05, 20th Annual IEEE Symposium on Logic in
Computer Science},
year = {2005},
pages = {},
publisher = {IEEE Computer Society Press},
}
XML Programming Languages and Webservices
G. Castagna, H. Im, K. Nguyễn, and V. Benzaken: A Core Calculus for XQuery 3.0. In ESOP '15: 24th European Symposium on Programming, n. 5710, LNCS, pag. 232-256, Springer, 2015. [Abstract] XML processing languages can be classified according to whether they
extract XML data by paths or pattern matching. In the former category
one finds XQuery, in the latter XDuce and CDuce. The
strengths of one category correspond to the weaknesses of the other.
In this work, we propose to bridge the gap between two of these
languages: XQuery and CDuce. We do it by extending CDuce so as it
can be seen as a succinct core lambda-calculus that
captures XQuery 3.0 programs. The extensions we consider essentially
allow CDuce to implement by pattern matching XPath-like navigation
expressions and to precisely type them. The encoding of XQuery 3.0
into the extension of CDuce provides a formal semantics and a sound
static type system for XQuery 3.0 programs.[BibTeX] Click for bibtex entry@inproceedings{CHNB15,
author = {G. Castagna and H. Im and K. Nguyễn and V. Benzaken},
title = {A Core Calculus for {XQuery} 3.0},
booktitle = {ESOP\,'15: 24th European Symposium on Programming},
year = {2015},
number = {5710},
series = {LNCS},
pages = {232-256},
publisher = {Springer},
}
G. Castagna, K. Nguyễn, Z. Xu, and P. Abate: Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. In POPL '15, 42nd ACM Symposium on Principles of Programming Languages, pag. 289―302, January, 2015. [Slides][Abstract] This article is the second part of a two articles series about
a calculus with higher-order polymorphic functions, recursive types
with arrow and product type constructors and set-theoretic type
connectives (union, intersection, and negation).
In the first part, presented in a companion paper, we defined and
studied the syntax, semantics, and evaluation of the explicitly-typed
version of the calculus, in which type instantiation is driven by
explicit instantiation annotations. In this second part we present a
local type inference system that allows the programmer to omit explicit
instantiation annotations, and a type reconstruction system that allows
the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations
and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce2,
author = {G. Castagna and K. Nguyễn and Z. Xu and P. Abate},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 2}: Local Type Inference and Type Reconstruction},
booktitle = {POPL\,'15, 42nd ACM Symposium on Principles of Programming Languages},
year = {2015},
pages = {289--302},
month = {jan},
}
G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, and L. Padovani: Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In POPL '14, 41st ACM Symposium on Principles of Programming Languages, pag. 5―17, January, 2014. [Slides][Abstract] This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation).
In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce1,
author = {G. Castagna and K. Nguyễn and Z. Xu and H. Im and S. Lenglet and L. Padovani},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 1}: Syntax, Semantics, and Evaluation},
booktitle = {POPL\,'14, 41st ACM Symposium on Principles of Programming Languages},
year = {2014},
pages = {5--17},
month = {jan},
}
G. Castagna and Z. Xu: Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, September, 2011. [Slides][Abstract] Working with XML data often yields to practical situations in which the programmer would need to assign parametric polymorphic types to higher-order functions.
However, up to date, there is no satisfactory way to do it. The
indirect purpose of this article is to define a system to remedy this lack. Its actual goal is to study parametric polymorphism for a type system with
recursive, product, union, intersection, negation, and function types
(the first three constructions are sufficient to encode XML types). We first
recall why the definition of such a system was considered hard―when
not impossible―and then present the main ideas at the basis
of our solution. In particular, we introduce the notion of
``convexity'' on which our solution is built up and discuss
its connections with parametricity as defined by
Reynolds to whose study our work sheds new light.[BibTeX] Click for bibtex entry@inproceedings{CX11,
author = {G. Castagna and Z. Xu},
title = {Set-theoretic Foundation of Parametric Polymorphism and Subtyping},
booktitle = {ICFP\,'11: 16th {ACM-SIGPLAN} International Conference on Functional Programming},
year = {2011},
pages = {94-106},
month = {sep},
}[Extended Version]
H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. ACM Transactions on Programming Languages and Systems, vol. 32, n. 1, pag. 1―56, 2009. [Abstract] Despite the extensiveness of recent investigations on static
typing for XML, parametric polymorphism has rarely been treated.
This well-established typing discipline can also be useful in
XML processing in particular for programs involving ``parametric
schemas,'' i.e., schemas parameterized over other schemas (e.g.,
SOAP). The difficulty in treating polymorphism for XML lies in
how to extend the ``semantic'' approach used in the mainstream
(monomorphic) XML type systems. A naive extension would be
``semantic'' quantification over all substitutions for type
variables. However, this approach reduces to an
NEXPTIME-complete problem for which no practical algorithm is
known. In this paper, we propose a different method that
smoothly extends the semantic approach yet is algorithmically
easier. In this, we devise a novel and simple marking technique, where we interpret a polymorphic type as a set of
values with annotations of which subparts are parameterized. We
exploit this interpretation in every ingredient of our
polymorphic type system such as subtyping, inference of type
arguments, and so on. As a result, we achieve a sensible system
that directly represents a usual expected behavior of
polymorphic type systems―``values of abstract types are never
reconstructed''―in a reminiscence of Reynold's parametricity
theory. Also, we obtain a set of practical algorithms for
typechecking by local modifications to existing ones for a
monomorphic system.[BibTeX] Click for bibtex entry@article{HFC09,
author = {H. Hosoya and A. Frisch and G. Castagna},
title = {Parametric Polymorphism for {XML}},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2009},
volume = {32},
number = {1},
pages = {1--56},
}
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems, vol. 31, n. 5, pag. 1―61, 2009. [Abstract] Contracts are behavioral descriptions of Web services. We devise a
theory of contracts that formalizes the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the
filter, which is an explicit coercion preventing some
possible behaviors of services and, in doing so, make services
compatible with different usage scenarios.
%
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatization of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We outline the practical aspects of our theory by
studying two different concrete syntaxes for contracts and applying each of
them to Web services languages. We also explore implementation issues
of filters and discuss the perspectives of future research this work opens.[BibTeX] Click for bibtex entry@article{CGP09,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2009},
volume = {31},
number = {5},
pages = {1--61},
note = {\ifFRENCH \'Etend et supplante~\cite{CGP08}\else Supersedes the article in POPL '08\fi},
}
V. Benzaken, G. Castagna, H. Hosoya, B.C. Pierce, and S. Vansummeren: The Encyclopedia of Database Systems, chapt. ``XML Typechecking'', Springer, 2009. ISBN 978-0-387-35544-3. [BibTeX]Click for bibtex entry@inbook{EDS,
author = {V. Benzaken and G. Castagna and H. Hosoya and B.C. Pierce and S. Vansummeren},
title = {The Encyclopedia of Database Systems},
chapter = {``{XML} Typechecking''},
publisher = {Springer},
year = {2009},
note = {ISBN 978-0-387-35544-3},
}
G. Castagna and K. Nguyễn: Typed Iterators for XML. In ICFP '08: 13th ACM-SIGPLAN International Conference on Functional Programming, pag. 15―26, April, 2008. [Abstract] XML transformations are very sensitive to types: XML types describe
the tags and attributes of XML elements as well as the number, kind,
and order of their sub-elements. Therefore, even very basic
operations such as changing a tag, renaming an attribute, or adding
an element generally imply conspicuous changes from the type of the
input to the type of the output. Such operations are applied on XML
documents by iterators that,
to be useful, need to be typed by some kind of polymorphism that
goes beyond what currently exists. For this reason these iterators
are not programmed but, rather, hard-coded in the language. However,
this approach soon reaches its limits, as the hard-coded iterators
cannot cover fairly standard usage scenarios.
As a solution to this problem we propose a generic language to define iterators
for XML data to be grafted on some host programming
language. We show that our language mostly offers the required
degree of polymorphism, study its formal properties, and show its
expressiveness and practical impact by providing several usage examples and encodings.[BibTeX] Click for bibtex entry@inproceedings{CN08icfp,
author = {G. Castagna and K. Nguyễn},
title = {Typed Iterators for {XML}},
booktitle = {ICFP '08: 13th {ACM-SIGPLAN} International Conference on Functional Programming},
year = {2008},
pages = {15--26},
month = {apr},
}
V. Benzaken, G. Castagna, D. Colazzo, and C. Miachon: Pattern by Example: type-driven visual programming of XML queries. In PPDP '08: 10th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming, pag. 131―142, ACM, 2008. [Abstract] We present Pattern-by-Example (PBE), a graphical language that allows
users with little or no knowledge of pattern-matching and functional programming
to define
complex and optimized queries on XML documents.
We demonstrate the key features of PBE by commenting an interactive
session and then we present its semantics, by formally defining a
translation from PBE graphical queries into CQL ones.
The advantages of the approach are twofold. First, it generates queries
that are provably correct with respect to types: the type of the result is
displayed to the user and this constitutes a first and immediate visual
check of the semantic correctness of the resulting query. The second
advantage is that a semantics formally―thus, unambiguously―defined is
an important advancement over some current approaches in which standard
usage and learning methods are based on ``trial and error'' techniques[BibTeX] Click for bibtex entry@inproceedings{BCM08,
author = {V. Benzaken and G. Castagna and D. Colazzo and C. Miachon},
title = {{Pattern by Example}: type-driven visual programming of {XML}
queries},
booktitle = {PPDP '08: 10th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming},
year = {2008},
pages = {131--142},
publisher = {ACM},
}
G. Castagna, N. Gesbert, and L. Padovani: A Theory of Contracts for Web Services. In POPL '08, 35th ACM Symposium on Principles of Programming Languages, pag. 261―272, January, 2008. [Abstract] Contracts are behavioural descriptions of Web services. We devise a
theory of contracts that formalises the compatibility of a client to a
service, and the safe replacement of a service with another service. The
use of contracts statically ensures the successful completion of every
possible interaction between compatible clients and services.
The technical device that underlies the theory is the definition of
filters, which are explicit coercions that prevent some
possible behaviours of services and, in doing so, they make services compatible
with different usage scenarios.
We show that filters can be seen as proofs of a sound and complete
subcontracting deduction system which simultaneously refines and extends
Hennessy's classical axiomatisation of the must testing preorder. The relation
is decidable and the decision algorithm is obtained via a cut-elimination
process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach
is based on simple ideas and basic intuitions. Remarkably, its application
is mostly independent of the language used to program the
services or the clients. We also outline the possible practical impact of such a
work and the perspectives of future research it opens.[BibTeX] Click for bibtex entry@inproceedings{CGP08,
author = {G. Castagna and N. Gesbert and L. Padovani},
title = {A Theory of Contracts for Web Services},
booktitle = {POPL~'08, 35th ACM Symposium on Principles of Programming Languages},
year = {2008},
pages = {261--272},
month = {jan},
}[Extended Version]
S. Carpineti, G. Castagna, C. Laneve, and L. Padovani: A formal account of contracts for Web Services. In WS-FM, 3rd Int. Workshop on Web Services and Formal Methods, n. 4184, LNCS, pag. 148-162, Springer, 2006. [Abstract] The Web Service Description Language (WSDL) and the Web Service Conversation
Language (WSCL) provide standard technologies for describing the static and
dynamic interfaces of Web services. In particular, they permit the
specification of the valid sequences of messages―the contract―required to
interact successfully with a Web service. However, neither of them provides
a formal definition of contract. We define a formal contract language along
with conformance and compliance relations so that clients conforming to a
contract are able to complete interactions with services compliant with the
same contract. Our contract language is suitable for publication in a WSDL
interface or as a WSCL resource. We take CCS as the formal model which our
investigation is based upon.[BibTeX] Click for bibtex entry@inproceedings{CCLP06,
author = {S. Carpineti and G. Castagna and C. Laneve and L. Padovani},
title = {A formal account of contracts for {Web} {S}ervices},
booktitle = {WS-FM, 3rd Int.\ Workshop on Web Services and Formal Methods},
year = {2006},
number = {4184},
series = {LNCS},
pages = {148-162},
publisher = {Springer},
}
G. Castagna, D. Colazzo, and A. Frisch: Error Mining for Regular Expression Patterns. In ICTCS 2005, Italian Conference on
Theoretical Computer Science, n. 3701, Lecture Notes in Computer Science, pag. 160-172, Springer, 2005. [Abstract] In the design of type systems for XML programming languages
based on regular expression types and patterns the focus has
been over result analysis, with the main aim of
statically checking that a transformation always yields data of
an expected output type. While being crucial for correct program
composition, result analysis is not sufficient to guarantee that
patterns used in the transformation are correct. In this paper
we motivate the need of static detection of incorrect patterns,
and provide a formal characterization based on pattern matching
operational semantics, together with locally exact type analysis
techniques to statically detect them.[BibTeX] Click for bibtex entry@inproceedings{CCF05,
author = {G. Castagna and D. Colazzo and A. Frisch},
title = {Error Mining for Regular Expression Patterns},
booktitle = {ICTCS 2005, Italian Conference on
Theoretical Computer Science},
year = {2005},
number = {3701},
series = {Lecture Notes in Computer Science},
pages = {160-172},
publisher = {Springer},
}
G. Castagna: Patterns and types for querying XML. In Proceedings of DBPL 2005, 10th International Symposium
on Database Programming Languages Lecture Notes
in Computer Science, n.3774, pages 1-26
Springer (full version) and XSym 2005, 3rd International
XML Database Symposium Lecture Notes
in Computer Science n.3671, pages 1-3,
Springer (summary), 2005. Joint DBPL-XSym invited talk. [Slides][Abstract] Among various proposals for primitives for deconstructing
XML data two approaches seem to clearly stem from practice: path
expressions, widely adopted by the database community, and
regular expression patterns, mainly developed and studied in the
programming language community. We think that the two approaches
are complementary and should be both integrated in languages for
XML, and we see in that an opportunity of collaboration between
the two communities. With this aim, we give a presentation of
regular expression patterns and the type systems they are
tightly coupled with. Although this article advocates a
construction promoted by the programming language community, we
will try to stress some characteristics that the database
community, we hope, may find interesting.[BibTeX] Click for bibtex entry@inproceedings{Cas05a,
author = {G. Castagna},
title = {Patterns and types for querying {XML}},
booktitle = {\emph{Proceedings of} DBPL 2005, 10th International Symposium
on Database Programming Languages \emph{Lecture Notes
in Computer Science, n.3774, pages 1-26
Springer (full version)} and XSym 2005, 3rd International
XML Database Symposium \emph {Lecture Notes
in Computer Science n.3671, pages 1-3,
Springer (summary)}},
year = {2005},
note = {Joint DBPL-XSym invited talk},
}
H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. In POPL '05, 32nd ACM Symposium on Principles of Programming Languages, pag. 50-62, ACM Press, 2005. [Abstract] Despite the extensiveness of recent investigations on static
typing for XML, parametric polymorphism has rarely been treated.
This well-established typing discipline can also be useful in
XML processing in particular for programs involving ``parametric
schemas,'' i.e., schemas parameterized over other schemas (e.g.,
SOAP). The difficulty in treating polymorphism for XML lies in
how to extend the ``semantic'' approach used in the mainstream
(monomorphic) XML type systems. A naive extension would be
``semantic'' quantification over all substitutions for type
variables. However, this approach reduces to an
NEXPTIME-complete problem for which no practical algorithm is
known. In this paper, we propose a different method that
smoothly extends the semantic approach yet is algorithmically
easier. In this, we devise a novel and simple marking technique, where we interpret a polymorphic type as a set of
values with annotations of which subparts are parameterized. We
exploit this interpretation in every ingredient of our
polymorphic type system such as subtyping, inference of type
arguments, and so on. As a result, we achieve a sensible system
that directly represents a usual expected behavior of
polymorphic type systems―``values of abstract types are never
reconstructed''―in a reminiscence of Reynold's parametricity
theory. Also, we obtain a set of practical algorithms for
typechecking by local modifications to existing ones for a
monomorphic system.[BibTeX] Click for bibtex entry@inproceedings{HFC05,
author = {H. Hosoya and A. Frisch and G. Castagna},
title = {Parametric Polymorphism for {XML}},
booktitle = {POPL~'05, 32nd ACM Symposium on Principles of Programming Languages},
year = {2005},
pages = {50-62},
publisher = {ACM Press},
}
V. Benzaken, G. Castagna, and C. Miachon: A Full Pattern-based Paradigm for XML Query Processing. In PADL 05, 7th International Symposium on
Practical Aspects of Declarative Languages, n. 3350, LNCS, pag. 235―252, Springer, January, 2005. [Abstract] In this article we investigate a novel execution
paradigm―ML-like pattern-matching―for XML query processing. We show that
such a paradigm is well adapted for a common and frequent set of queries and
advocate that it constitutes a candidate for efficient execution of XML queries
far better than the current XPath-based query mechanisms. We support our claim by
comparing performances of XPath-based queries with pattern based ones, and by
comparing the latter with the two efficiency-best XQuery processor we are aware
of.[BibTeX] Click for bibtex entry@inproceedings{BCM05,
author = {V. Benzaken and G. Castagna and C. Miachon},
title = {A Full Pattern-based Paradigm for {XML} Query Processing},
booktitle = {PADL~05, 7th International Symposium on
Practical Aspects of Declarative Languages},
year = {2005},
number = {3350},
series = {LNCS},
pages = {235--252},
month = {jan},
publisher = {Springer},
}
V. Benzaken, M. Burelle, and G. Castagna: Information flow security for XML transformations. In ASIAN '03, 8th Asian Computing Science Conference, n. 2896, LNCS, pag. 33-53, Springer, December, 2003. [Abstract] We provide a formal definition of information flows in XML
transformations and, more generally, in the presence of type
driven computations and describe a sound technique to detect
transformations that may leak private or confidential
information. We also outline a general framework to check
middleware-located information flows.[BibTeX] Click for bibtex entry@inproceedings{BBC03,
author = {V. Benzaken and M. Burelle and G. Castagna},
title = {Information flow security for {XML} transformations},
booktitle = {ASIAN '03, 8th Asian Computing Science Conference},
year = {2003},
number = {2896},
series = {LNCS},
pages = {33-53},
month = {dec},
publisher = {Springer},
}
V. Benzaken, G. Castagna, and A. Frisch: CDuce: an XML-Centric General-Purpose Language. In ICFP '03, 8th ACM International Conference on Functional Programming, pag. 51―63, ACM Press, 2003. [Abstract] We present the functional language ℂDuce, discuss some
design issues, and show its adequacy for working with XML
documents. Distinctive features of ℂDuce are a powerful
pattern matching, first class functions, overloaded functions, a
very rich type system (arrows, sequences, pairs, records,
intersections, unions, differences), precise type inference for
patterns and error localization, and a natural interpretation of
types as sets of values. We also outline some important
implementation issues; in particular, a dispatch algorithm that
demonstrates how static type information can be used to obtain
very efficient compilation schemas.[BibTeX] Click for bibtex entry@inproceedings{BCF03,
author = {V. Benzaken and G. Castagna and A. Frisch},
title = {{CD}uce: an {XML}-Centric General-Purpose Language},
booktitle = {ICFP~'03, 8th ACM International Conference on Functional Programming},
year = {2003},
pages = {51--63},
address = {Uppsala, Sweden},
publisher = {ACM Press},
}
A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping. In LICS '02, 17th Annual IEEE Symposium on Logic in
Computer Science, pag. 137―146, IEEE Computer Society Press, 2002. [Abstract] Usually subtyping relations are defined either syntactically by a
formal system or semantically by an interpretation of types in
an untyped denotational model. In this work we show how to
define a subtyping relation semantically, for a language whose
operational semantics is driven by types; we
consider a rich type algebra, with product, arrow, recursive,
intersection, union and complement types. Our approach is to
``bootstrap'' the subtyping relation through a notion of
set-theoretic model of the type algebra.
The advantages of the semantic approach are manifold. Foremost
we get ``for free'' many properties (e.g., the transitivity of
subtyping) that, with axiomatized subtyping, would require
tedious and error prone proofs. Equally important is that the
semantic approach allows one to derive complete
algorithms for the subtyping relation or the propagation of
types through patterns. As the subtyping relation has a natural
(inasmuch as semantic) interpretation, the type system can give
informative error messages when static type-checking fails.
Last but not least the approach has an immediate impact in the
definition and the implementation of languages
manipulating XML documents, as this was our original
motivation.[BibTeX] Click for bibtex entry@inproceedings{FCB02,
author = {A. Frisch and G. Castagna and V. Benzaken},
title = {Semantic {S}ubtyping},
booktitle = {LICS '02, 17th Annual IEEE Symposium on Logic in
Computer Science},
year = {2002},
pages = {137--146},
publisher = {IEEE Computer Society Press},
}
G. Castagna, J. Demouth, A. Frisch, and S. Zacchiroli: ℂDuce User Manual, 2002-2015. Available on line at http://www.cduce.org/manual.html. [BibTeX]Click for bibtex entry@manual{cduceUM,
author = {G. Castagna and J. Demouth and A. Frisch and S. Zacchiroli},
title = {\cduce{} User Manual},
year = {2002-2015},
note = {Available on line at \url{http://www.cduce.org/manual.html}},
}
V. Benzaken, G. Castagna, and A. Frisch: ℂDuce Tutorial, 2002-2015. Available on line at http://www.cduce.org/tutorial.html. [BibTeX]Click for bibtex entry@manual{cduceTutorial,
author = {V. Benzaken and G. Castagna and A. Frisch},
title = {\cduce{} Tutorial},
year = {2002-2015},
note = {Available on line at \url{http://www.cduce.org/tutorial.html}},
}
Mobility and Distribution
G. Castagna, J. Vitek, and F. Zappa Nardelli: The Seal Calculus. Information and Computation, vol. 201, n. 1, pag. 1―54, 2005. [Abstract] The Seal Calculus is a process language for describing mobile
computation. Threads and resources are tree structured; the
nodes thereof correspond to agents, the units of mobility. The
Calculus extends a π-calculus core with synchronous,
objective mobility of agents over channels. This paper
systematically compares all previous variants of Seal Calculus.
We study their operational behaviour with labelled transition
systems and bisimulations; by comparing the resulting algebraic
theories we highlight the differences between these
apparently similar approaches. This leads us to identify the
dialect of Seal that is most amenable to operational reasoning
and can form the basis of a distributed programming language.
We propose type systems for characterising the communications in
which an agent can engage. The type systems thus enforce a
discipline of agent mobility, since the latter is coded in terms
of higher-order communication.[BibTeX] Click for bibtex entry@article{CVZ05,
author = {G. Castagna and J. Vitek and F. Zappa~Nardelli},
title = {The {S}eal {C}alculus},
journal = {Information and Computation},
year = {2005},
volume = {201},
number = {1},
pages = {1--54},
}
M. Bugliesi, G. Castagna, and S. Crafa: Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems, vol. 26, n. 1, pag. 57-124, 2004. [BCC01a,BCC01b]. [Abstract] Boxed Ambients are a variant of Mobile Ambients
that result from dropping the open capability, and
introducing new primitives for ambient communication. The new
model of communication is faithful to the principles of
distribution and location-awareness of Mobile Ambients, and
complements the constructs in and out for
mobility with finer-grained mechanisms for ambient interaction.
We introduce the new calculus, study the impact of the new
mechanisms for communication o typing and mobility, and show
that they yield an effective framework for resource protection
and access control in distributed systems.[BibTeX] Click for bibtex entry@article{BCC04,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Access Control for Mobile Agents: The {Calculus} of {Boxed} {Ambients}},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2004},
volume = {26},
number = {1},
pages = {57-124},
note = {\ifFRENCH Inclut et {é}tend les resultats de\else Includes and extends\fi~\cite{BCC01a,BCC01b}},
}
G. Castagna and F. Zappa Nardelli: The Seal Calculus revisited: contextual equivalence and bisimilarity. In FST&TCS '02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science, n. 2556, LNCS, pag. 85―96, Springer, December, 2002. [Abstract] We present a new version of the Seal Calculus,
a calculus of mobile computation. We study observational
congruence and bisimulation theory, and show how they
are related.[BibTeX] Click for bibtex entry@inproceedings{CZ02,
author = {G. Castagna and F. {Zappa Nardelli}},
title = {The {Seal} {Calculus} revisited: contextual equivalence and bisimilarity},
booktitle = {{FST\&TCS} '02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science},
year = {2002},
number = {2556},
series = {LNCS},
pages = {85--96},
month = {dec},
publisher = {Springer},
}
Crafa, S., Bugliesi, M., and Castagna, G.: Information Flow Security for Boxed Ambients. In Foundations of Wide Area Network Computing (F-WAN), n. 66(3), Electronic Notes in Theoretical Computer Science, Elsevier Science B.V., 2002. [Abstract] We study the problem of secure information flow for Boxed
Ambients in terms of non-interference. The main contribution of
this work is the study and the (type-based) control of new
sources of information flow due to the interplay between
communication and mobility, which is typical of network
programming. We develop a sound type system that provides
static guarantees of absence of unwanted flow of information for
well typed processes. Non-interference is stated, and proved, in
terms of a typed notion of contextual equivalence for Boxed
Ambients akin to the corresponding equivalence defined for
Mobile Ambients.[BibTeX] Click for bibtex entry@inproceedings{CBC02,
author = {Crafa, S. and Bugliesi, M. and Castagna, G.},
title = {Information Flow Security for {B}oxed {A}mbients},
booktitle = {Foundations of Wide Area Network Computing (F-WAN)},
year = {2002},
number = {66(3)},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science B.V.},
}
M. Bugliesi and G. Castagna: Behavioral Typing for Safe Ambients. Computer Languages, vol. 28, n. 1, pag. 61-99, November, 2002. [Abstract] We introduce a typed variant of Safe Ambients,
named Secure Safe Ambients (SSA), whose type system
allows behavioral invariants of ambients to be expressed and
verified. The most significant aspect of the type system is its
ability to capture both explicit and implicit process and ambient behavior: process types account not
only for immediate behavior, but also for the behavior resulting
from capabilities a process acquires during its evolution in a
given context. Based on that, the type system provides for
static detection of security attacks such as Trojan
Horses and other combinations of malicious agents.
We study the type system of SSA, define algorithms for type
checking and type reconstruction, define languages for
expressing security properties, and study a distributed version
of SSA and its type system. For the latter, we show that
distributed type checking ensures security even in ill-typed
contexts, and discuss how it relates to the security
architecture of the Java Virtual Machine.[BibTeX] Click for bibtex entry@article{BCcl,
author = {M. Bugliesi and G. Castagna},
title = {Behavioral Typing for {S}afe {A}mbients},
journal = {Computer Languages},
year = {2002},
volume = {28},
number = {1},
pages = {61-99},
month = {nov},
}
G. Castagna: An overview of Boxed Ambients. In TOSCA '01, Theory of Concurrency, Higher Order, and Types Workshop, n. 62, Electronic Notes in Theoretical Computer Science, pag. 1-5, Elsevier Science B.V., 2001. Invited lecture based on joint work with M. Bugliesi and S. Crafa: [BCC01a,BCC01b]. [Abstract] In this lecture we present some work we did about mobility and
hint at some new current lines of research on information flow and security.
More precisely, we describe the calculus of Boxed
Ambients a variant of Cardelli and Gordon's Mobile
Ambients a calculus of mobile and dynamically
reconfigurable agents. Boxed Ambients inherit from Mobile
Ambients (part of) the mobility primitives but rely on a
completely different model of communication. The new
communication primitives fit nicely the design principles of
Mobile Ambients, and complement the existing constructs for
ambient mobility with finer-grained, and more effective,
mechanisms for ambient interaction. As a result Boxed Ambients
retain the expressive power and the computational flavor of
Ambient Calculus, as well as the elegance of its formal
presentation. In addition, they enhance the flexibility of typed
communications over Mobile Ambients, and provide new insight
into the relationship between synchronous and asynchronous
input-output.[BibTeX] Click for bibtex entry@inproceedings{Cas01,
author = {G. Castagna},
title = {An overview of {B}oxed {A}mbients},
booktitle = {{TOSCA} '01, Theory of Concurrency, Higher Order, and Types Workshop},
year = {2001},
number = {62},
series = {Electronic Notes in Theoretical Computer Science},
pages = {1-5},
publisher = {Elsevier Science B.V.},
note = {Invited lecture based on joint work with M.~Bugliesi and S.~Crafa:~\cite{BCC01a,BCC01b}},
}
M. Bugliesi, G. Castagna, and S. Crafa: Reasoning about security in Mobile Ambients. In CONCUR 2001, 12th. International
Conference on Concurrency Theory, n. 2154, LNCS, pag. 102-120, Springer, 2001. Contained in [BCC04]. [Abstract] The paper gives an assessment of security for Mobile
Ambients, with specific focus on mandatory access
control (MAC) policies in multilevel security systems.
The first part of the paper reports on different formalization
attempts for MAC policies in the Ambient Calculus, and provides
an in-depth analysis of the problems one encounters. As it turns
out, MAC security does not appear to have fully convincing
interpretations in the calculus.
The second part proposes a solution to this impasse,
based on a variant of Mobile Ambients. A type system for
resource access control is defined, and the new calculus is
discussed and illustrated with several examples of resource
management policies.[BibTeX] Click for bibtex entry@inproceedings{BCC01b,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Reasoning about security in Mobile Ambients},
booktitle = {{CONCUR} 2001, 12th.\ International
Conference on Concurrency Theory},
year = {2001},
number = {2154},
series = {LNCS},
pages = {102-120},
address = {Aahrus, Danemark},
publisher = {Springer},
note = {Contained in~\cite{BCC04}},
}
M. Bugliesi, G. Castagna, and S. Crafa: Boxed Ambients. In TACS 2001, 4th. International Symposium on
Theoretical Aspects of Computer Science, n. 2215, LNCS, pag. 38―63, Springer, 2001. Contained in [BCC04]. [Abstract] Boxed Ambients are a variant of Mobile Ambients,
that result from (i) dropping the open capability and (ii) providing new primitives for ambient
communication while retaining the constructs in and out for mobility. The new model of
communication is faithful to the principles of distribution
and location-awareness of Mobile Ambients, and complements
the constructs for Mobile Ambient mobility with
finer-grained, and more effective, mechanisms for ambient
interaction.[BibTeX] Click for bibtex entry@inproceedings{BCC01a,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Boxed Ambients},
booktitle = {{TACS} 2001, 4th.\ International Symposium on
Theoretical Aspects of Computer Science},
year = {2001},
number = {2215},
series = {LNCS},
pages = {38--63},
address = {Sendai, Japan},
publisher = {Springer},
note = {Contained in~\cite{BCC04}},
}
M. Bugliesi, G. Castagna, and S. Crafa: Subtyping and Matching for Mobile Objects. In ICTCS 2001, 7th. Italian
Conference on Theoretical Computer Science, n. 2202, LNCS, pag. 235―255, Springer, 2001. [Abstract] In a previous work we presented a general framework for
extending calculi of mobile agents with object-oriented
features, and we studied a typed instance of that model based on
Cardelli and Gordon's Mobile Ambients. Here, we refine our
earlier work and define a new calculus which is based on
Remote Procedure Call as the underlying protocol for
method invocation, and on a different typing technique for
method bodies. The new type system is equipped with a subtyping
and a matching relation: the combination of matching with
subtyping provides new insight into the relationship between
ambient opening in the new calculus and method overriding in
object-oriented calculi.[BibTeX] Click for bibtex entry@inproceedings{BCC01c,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Subtyping and Matching for Mobile Objects},
booktitle = {{ICTCS} 2001, 7th.\ Italian
Conference on Theoretical Computer Science},
year = {2001},
number = {2202},
series = {LNCS},
pages = {235--255},
address = {Torino, Italy},
publisher = {Springer},
}
G. Castagna, G. Ghelli, and F. Zappa Nardelli: Typing Mobility in the Seal Calculus. In CONCUR 2001, 12th. International
Conference on Concurrency Theory, n. 2154, LNCS, pag. 82-101, Springer, 2001. [Abstract] The issue of this work is how to type mobility, in the sense
that we tackle the problem of typing not only mobile agents but
also their movement. This yields higher-order types for agents.
To that end we first provide a new definition of the Seal
Calculus that gets rid of existing inessential features while
preserving the distinctive characteristics of the Seal
model. Then we discuss the use of interfaces to type agents and
define the type system. The interpretation induced by this type
system is that interfaces describe interaction effects rather than, as it is customary, provided services. We
discuss at length the difference of the two interpretations and
justify our choice of the former.[BibTeX] Click for bibtex entry@inproceedings{CGZ01,
author = {G. Castagna and G. Ghelli and F. {Zappa Nardelli}},
title = {Typing Mobility in the {S}eal {C}alculus},
booktitle = {{CONCUR} 2001, 12th.\ International
Conference on Concurrency Theory},
year = {2001},
number = {2154},
series = {LNCS},
pages = {82-101},
address = {Aahrus, Danemark},
publisher = {Springer},
}
M. Bugliesi and G. Castagna: Secure Safe Ambients. In POPL '01, 28th ACM Symposium on Principles of Programming Languages, pag. 222-235, ACM Press, 2001. Contained in [BCcl]. [Abstract] Secure Safe Ambients (SSA) are a typed variant of
Safe Ambients, whose type system allows
behavioral invariants of ambients to be expressed and verified.
The most significant aspect of the type system is its ability to
capture both explicit and implicit process and
ambient behavior: process types account not only for immediate
behavior, but also for the behavior resulting from capabilities
a process acquires during its evolution in a given context.
Based on that, the type system provides for static detection of
security attacks such as Trojan Horses and other
combinations of malicious agents.
We study the type system of SSA, define algorithms for type
checking and type reconstruction, define powerful languages for
expressing security properties, and study a distributed version
of SSA and its type system. For the latter, we show that
distributed type checking ensures security even in ill-typed
contexts, and discuss how it relates to the security
architecture of the Java Virtual Machine.[BibTeX] Click for bibtex entry@inproceedings{BC01,
author = {M. Bugliesi and G. Castagna},
title = {Secure Safe Ambients},
booktitle = {POPL '01, 28th ACM Symposium on Principles of Programming Languages},
year = {2001},
pages = {222-235},
address = {London},
publisher = {ACM Press},
note = {Contained in~\cite{BCcl}},
}
M. Bugliesi, G. Castagna, and S. Crafa: Typed Mobile Objects. In CONCUR 2000, 11th. International
Conference on Concurrency Theory, n. 1877, LNCS, pag. 504-520, Springer, 2000. [BibTeX]Click for bibtex entry@inproceedings{BCC00,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Typed Mobile Objects},
booktitle = {{CONCUR} 2000, 11th.\ International
Conference on Concurrency Theory},
year = {2000},
number = {1877},
series = {LNCS},
pages = {504-520},
address = {Penn State University Parc},
publisher = {Springer},
}
G. Castagna and J. Vitek: Seal: A Framework for Secure Mobile Computations. In Internet Programming Languages, Springer, n. 1686, LNCS, pag. 47-77, 1999. Collected works. [BibTeX]Click for bibtex entry@incollection{CV99,
author = {G. Castagna and J. Vitek},
title = {Seal: A Framework for Secure Mobile Computations},
booktitle = {Internet Programming Languages},
publisher = {Springer},
year = {1999},
editor = {H. Bal and B. Belkhouche and L. Cardelli},
number = {1686},
series = {LNCS},
pages = {47-77},
note = {Collected works\ifFRENCH\ [modalit{é}s de s{é}lection d'un num{é}ro sp{é}cial de revue. Assimilable {à} un article de revue internationale avec comit{é} de lecture]\else\fi},
}
G. Castagna: Types et Modèles : des langages objets séquentiels à la mobilité et à la sécurité, Université Paris 7, Habilitation à diriger des recherches, January, 2002. [BibTeX]Click for bibtex entry@phdthesis{Cas02hab,
author = {G. Castagna},
title = {Types et {M}od{è}les : des langages objets s{é}quentiels {à} la mobilit{é} et {à} la s{é}curit{é}},
school = {Universit{é} Paris 7},
year = {2002},
type = {Habilitation {à} diriger des recherches},
month = {jan},
}
Databases
V. Benzaken, G. Castagna, L. Daynes, J. Lopez, K. Nguyen, and R. Vernoux: Language-integrated queries: a BOLDR approach. In Proceedings of the Web Conference (WWW2018), Web Programming track, April, 2018. [Abstract] We present BOLDR, a modular framework that enables the evaluation in, databases of queries containing application logic and, in particular,, user-defined functions. BOLDR also allows the nesting of queries for different, databases of possibly different data models. The framework detects the, boundaries of queries present in an application, translates them into an, intermediate representation together with the relevant language environment,, rewrites them in order to avoid query avalanches and to make the most out of, database optimizations, and converts the results back to the application. We, also present experiments showing that the techniques we implemented are, applicable to real-world database applications, both in terms of successfully, handling different sorts of language-integrated queries, and in terms of, better performance.[BibTeX] Click for bibtex entry@inproceedings{boldr,
author = {V. Benzaken and G. Castagna and L. Daynes and J. Lopez and K. Nguyen and R. Vernoux},
title = {Language-integrated queries: a {BOLDR} approach},
booktitle = {Proceedings of the Web Conference ({WWW2018}), Web Programming track},
year = {2018},
month = {apr},
}
G. Castagna, H. Im, K. Nguyễn, and V. Benzaken: A Core Calculus for XQuery 3.0. In ESOP '15: 24th European Symposium on Programming, n. 5710, LNCS, pag. 232-256, Springer, 2015. [Abstract] XML processing languages can be classified according to whether they
extract XML data by paths or pattern matching. In the former category
one finds XQuery, in the latter XDuce and CDuce. The
strengths of one category correspond to the weaknesses of the other.
In this work, we propose to bridge the gap between two of these
languages: XQuery and CDuce. We do it by extending CDuce so as it
can be seen as a succinct core lambda-calculus that
captures XQuery 3.0 programs. The extensions we consider essentially
allow CDuce to implement by pattern matching XPath-like navigation
expressions and to precisely type them. The encoding of XQuery 3.0
into the extension of CDuce provides a formal semantics and a sound
static type system for XQuery 3.0 programs.[BibTeX] Click for bibtex entry@inproceedings{CHNB15,
author = {G. Castagna and H. Im and K. Nguyễn and V. Benzaken},
title = {A Core Calculus for {XQuery} 3.0},
booktitle = {ESOP\,'15: 24th European Symposium on Programming},
year = {2015},
number = {5710},
series = {LNCS},
pages = {232-256},
publisher = {Springer},
}
V. Benzaken, G. Castagna, K. Nguyễn, and J. Siméon: Static and Dynamic Semantics of NoSQL Languages. In POPL '13, 40th ACM Symposium on Principles of Programming Languages, pag. 101―113, 2013. [Abstract] We present a calculus for processing semistructured data that spans
differences of application area among several novel query lan- guages, broadly categorized as “NoSQL”. This calculus lets users
define their own operators, capturing a wider range of data processing capabilities, whilst providing a typing precision so far typical
only of primitive hard-coded operators. The type inference algorithm is based on semantic type checking, resulting in type infor- mation that is both precise, and flexible enough to handle structured
and semistructured data. We illustrate the use of this calculus by
encoding a large fragment of Jaql, including operations and iterators over JSON, embedded SQL expressions, and co-grouping, and
show how the encoding directly yields a typing discipline for Jaql
as it is, namely without the addition of any type definition or type
annotation in the code.[BibTeX] Click for bibtex entry@inproceedings{BCNS13,
author = {V. Benzaken and G. Castagna and K. Nguyễn and J. Siméon},
title = {Static and Dynamic Semantics of {NoSQL} Languages},
booktitle = {POPL\,'13, 40th ACM Symposium on Principles of Programming Languages},
year = {2013},
pages = {101--113},
}[Extended Version]
V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyễn: Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems, vol. 38, n. 1, pag. 4:1―4:45, 2013. [Abstract] XML data projection (or pruning) is a natural
optimization for main memory query engines: given a
query Q over a document D, the subtrees of D that
are not necessary to evaluate Q are pruned, thus
producing a smaller document D ; the query Q is then
executed on D , hence avoiding to allocate and
process nodes that will never be reached by Q. In
this article, we propose a new approach, based on
types, that greatly improves current solutions.
Besides providing comparable or greater precision
and far lesser pruning overhead, our solution
―unlike current approaches― takes into account
backward axes, predicates, and can be applied to
multiple queries rather than just to single ones. A
side contribution is a new type system for XPath
able to handle backward axes. The soundness of our
approach is formally proved. Furthermore, we prove
that the approach is also complete (i.e., yields the
best possible type-driven pruning) for a relevant
class of queries and Schemas. We further validate
our approach using the XMark and XPathMark
benchmarks and show that pruning not only improves
the main memory query engine's performances (as
expected) but also those of state of the art native
XML databases.[BibTeX] Click for bibtex entry@article{BCCN13,
author = {V. Benzaken and G. Castagna and D. Colazzo and K. Nguyễn},
title = {Optimizing {XML} querying using type-based document projection},
journal = {ACM Transactions on Database Systems},
year = {2013},
volume = {38},
number = {1},
pages = {4:1--4:45},
}
V. Benzaken, G. Castagna, D. Colazzo, and C. Miachon: Pattern by Example: type-driven visual programming of XML queries. In PPDP '08: 10th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming, pag. 131―142, ACM, 2008. [Abstract] We present Pattern-by-Example (PBE), a graphical language that allows
users with little or no knowledge of pattern-matching and functional programming
to define
complex and optimized queries on XML documents.
We demonstrate the key features of PBE by commenting an interactive
session and then we present its semantics, by formally defining a
translation from PBE graphical queries into CQL ones.
The advantages of the approach are twofold. First, it generates queries
that are provably correct with respect to types: the type of the result is
displayed to the user and this constitutes a first and immediate visual
check of the semantic correctness of the resulting query. The second
advantage is that a semantics formally―thus, unambiguously―defined is
an important advancement over some current approaches in which standard
usage and learning methods are based on ``trial and error'' techniques[BibTeX] Click for bibtex entry@inproceedings{BCM08,
author = {V. Benzaken and G. Castagna and D. Colazzo and C. Miachon},
title = {{Pattern by Example}: type-driven visual programming of {XML}
queries},
booktitle = {PPDP '08: 10th international ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming},
year = {2008},
pages = {131--142},
publisher = {ACM},
}
V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyễn: Type-Based XML Projection. In VLDB 2006, 32nd International Conference on Very Large Data Bases, pag. 271-282, 2006. [Abstract] XML data projection (or pruning) is one of the main
optimization techniques recently adopted in the context of
main-memory XML query-engines. The underlying idea is quite
simple: given a query Q over a document D, the subtrees of
D not necessary to evaluate Q are pruned, thus obtaining a
smaller document D'. Then Q is executed over D', hence
avoiding to allocate and process nodes that will never be
reached by navigational specifications in Q.
In this article, we propose a new approach, based on types, that
greatly improves current solutions. Besides providing
comparable or greater precision and far lesser pruning overhead
our solution, unlike current approaches, takes into account
backward axes, predicates, and can be applied to multiple
queries rather than just to single ones. A side contribution is
a new type system for XPath able to handle backward axes, which
we devise in order to apply our solution.
The soundness of our approach is formally proved. Furthermore,
we prove that the approach is also complete (i.e., yields the
best possible type-driven pruning) for a relevant class of
queries and DTDs, which include nearly all the queries used in
the XMark and XPathMark benchmarks. These benchmarks are also
used to test our implementation and show and gauge the practical
benefits of our solution.[BibTeX] Click for bibtex entry@inproceedings{BCCN06,
author = {V. Benzaken and G. Castagna and D. Colazzo and K. Nguyễn},
title = {Type-Based {XML} Projection},
booktitle = {VLDB 2006, 32nd International Conference on Very Large Data Bases},
year = {2006},
pages = {271-282},
}
G. Castagna: Patterns and types for querying XML. In Proceedings of DBPL 2005, 10th International Symposium
on Database Programming Languages Lecture Notes
in Computer Science, n.3774, pages 1-26
Springer (full version) and XSym 2005, 3rd International
XML Database Symposium Lecture Notes
in Computer Science n.3671, pages 1-3,
Springer (summary), 2005. Joint DBPL-XSym invited talk. [Slides][Abstract] Among various proposals for primitives for deconstructing
XML data two approaches seem to clearly stem from practice: path
expressions, widely adopted by the database community, and
regular expression patterns, mainly developed and studied in the
programming language community. We think that the two approaches
are complementary and should be both integrated in languages for
XML, and we see in that an opportunity of collaboration between
the two communities. With this aim, we give a presentation of
regular expression patterns and the type systems they are
tightly coupled with. Although this article advocates a
construction promoted by the programming language community, we
will try to stress some characteristics that the database
community, we hope, may find interesting.[BibTeX] Click for bibtex entry@inproceedings{Cas05a,
author = {G. Castagna},
title = {Patterns and types for querying {XML}},
booktitle = {\emph{Proceedings of} DBPL 2005, 10th International Symposium
on Database Programming Languages \emph{Lecture Notes
in Computer Science, n.3774, pages 1-26
Springer (full version)} and XSym 2005, 3rd International
XML Database Symposium \emph {Lecture Notes
in Computer Science n.3671, pages 1-3,
Springer (summary)}},
year = {2005},
note = {Joint DBPL-XSym invited talk},
}
V. Benzaken, G. Castagna, and C. Miachon: A Full Pattern-based Paradigm for XML Query Processing. In PADL 05, 7th International Symposium on
Practical Aspects of Declarative Languages, n. 3350, LNCS, pag. 235―252, Springer, January, 2005. [Abstract] In this article we investigate a novel execution
paradigm―ML-like pattern-matching―for XML query processing. We show that
such a paradigm is well adapted for a common and frequent set of queries and
advocate that it constitutes a candidate for efficient execution of XML queries
far better than the current XPath-based query mechanisms. We support our claim by
comparing performances of XPath-based queries with pattern based ones, and by
comparing the latter with the two efficiency-best XQuery processor we are aware
of.[BibTeX] Click for bibtex entry@inproceedings{BCM05,
author = {V. Benzaken and G. Castagna and C. Miachon},
title = {A Full Pattern-based Paradigm for {XML} Query Processing},
booktitle = {PADL~05, 7th International Symposium on
Practical Aspects of Declarative Languages},
year = {2005},
number = {3350},
series = {LNCS},
pages = {235--252},
month = {jan},
publisher = {Springer},
}
Bioinformatics
A. Phillips, L. Cardelli, and G. Castagna: A Graphical Representation for Biological Processes in the Stochastic pi-calculus. Transactions on Computational Systems Biology, vol. 7, pag. 123-152, 2006. [Abstract] This paper presents a graphical representation for the stochastic
pi-calculus, which is formalised by defining a corresponding graphical
calculus. The graphical calculus is shown to be reduction equivalent to
stochastic pi, ensuring that the two calculi have the same expressive
power. The graphical representation is used to model a couple of example
biological systems, namely a bistable gene network and a mapk signalling
cascade. One of the main benefits of the representation is its ability to
highlight the existence of cycles, which are a key feature of many biological
systems. Another benefit is its ability to animate interactions between
system components, in order to visualise system dynamics. The graphical
representation can also be used as a front end to a simulator for the
stochastic pi-calculus, with a view to making modelling and simulation of
biological systems more accessible to non computer scientists.[BibTeX] Click for bibtex entry@article{PCC06,
author = {A. Phillips and L. Cardelli and G. Castagna},
title = {A Graphical Representation for Biological Processes in the Stochastic pi-calculus},
journal = {Transactions on Computational Systems Biology},
year = {2006},
volume = {7},
pages = {123-152},
}
Security
M. Bugliesi, G. Castagna, and S. Crafa: Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems, vol. 26, n. 1, pag. 57-124, 2004. [BCC01a,BCC01b]. [Abstract] Boxed Ambients are a variant of Mobile Ambients
that result from dropping the open capability, and
introducing new primitives for ambient communication. The new
model of communication is faithful to the principles of
distribution and location-awareness of Mobile Ambients, and
complements the constructs in and out for
mobility with finer-grained mechanisms for ambient interaction.
We introduce the new calculus, study the impact of the new
mechanisms for communication o typing and mobility, and show
that they yield an effective framework for resource protection
and access control in distributed systems.[BibTeX] Click for bibtex entry@article{BCC04,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Access Control for Mobile Agents: The {Calculus} of {Boxed} {Ambients}},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2004},
volume = {26},
number = {1},
pages = {57-124},
note = {\ifFRENCH Inclut et {é}tend les resultats de\else Includes and extends\fi~\cite{BCC01a,BCC01b}},
}
M. Bugliesi, G. Castagna, S. Crafa, R. Focardi, and V. Sassone: Name-passing calculi and crypto-primitives: a survey. In Foundations of Security Analysis and Design, n. 2946, LNCS, pag. 91-138, Springer, 2004. [BibTeX]Click for bibtex entry@inproceedings{BCCFS04,
author = {M. Bugliesi and G. Castagna and S. Crafa and R. Focardi and V. Sassone},
title = {Name-passing calculi and crypto-primitives: a survey},
booktitle = {Foundations of Security Analysis and Design},
year = {2004},
number = {2946},
series = {LNCS},
pages = {91-138},
publisher = {Springer},
}
V. Benzaken, M. Burelle, and G. Castagna: Information flow security for XML transformations. In ASIAN '03, 8th Asian Computing Science Conference, n. 2896, LNCS, pag. 33-53, Springer, December, 2003. [Abstract] We provide a formal definition of information flows in XML
transformations and, more generally, in the presence of type
driven computations and describe a sound technique to detect
transformations that may leak private or confidential
information. We also outline a general framework to check
middleware-located information flows.[BibTeX] Click for bibtex entry@inproceedings{BBC03,
author = {V. Benzaken and M. Burelle and G. Castagna},
title = {Information flow security for {XML} transformations},
booktitle = {ASIAN '03, 8th Asian Computing Science Conference},
year = {2003},
number = {2896},
series = {LNCS},
pages = {33-53},
month = {dec},
publisher = {Springer},
}
Crafa, S., Bugliesi, M., and Castagna, G.: Information Flow Security for Boxed Ambients. In Foundations of Wide Area Network Computing (F-WAN), n. 66(3), Electronic Notes in Theoretical Computer Science, Elsevier Science B.V., 2002. [Abstract] We study the problem of secure information flow for Boxed
Ambients in terms of non-interference. The main contribution of
this work is the study and the (type-based) control of new
sources of information flow due to the interplay between
communication and mobility, which is typical of network
programming. We develop a sound type system that provides
static guarantees of absence of unwanted flow of information for
well typed processes. Non-interference is stated, and proved, in
terms of a typed notion of contextual equivalence for Boxed
Ambients akin to the corresponding equivalence defined for
Mobile Ambients.[BibTeX] Click for bibtex entry@inproceedings{CBC02,
author = {Crafa, S. and Bugliesi, M. and Castagna, G.},
title = {Information Flow Security for {B}oxed {A}mbients},
booktitle = {Foundations of Wide Area Network Computing (F-WAN)},
year = {2002},
number = {66(3)},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science B.V.},
}
M. Bugliesi and G. Castagna: Behavioral Typing for Safe Ambients. Computer Languages, vol. 28, n. 1, pag. 61-99, November, 2002. [Abstract] We introduce a typed variant of Safe Ambients,
named Secure Safe Ambients (SSA), whose type system
allows behavioral invariants of ambients to be expressed and
verified. The most significant aspect of the type system is its
ability to capture both explicit and implicit process and ambient behavior: process types account not
only for immediate behavior, but also for the behavior resulting
from capabilities a process acquires during its evolution in a
given context. Based on that, the type system provides for
static detection of security attacks such as Trojan
Horses and other combinations of malicious agents.
We study the type system of SSA, define algorithms for type
checking and type reconstruction, define languages for
expressing security properties, and study a distributed version
of SSA and its type system. For the latter, we show that
distributed type checking ensures security even in ill-typed
contexts, and discuss how it relates to the security
architecture of the Java Virtual Machine.[BibTeX] Click for bibtex entry@article{BCcl,
author = {M. Bugliesi and G. Castagna},
title = {Behavioral Typing for {S}afe {A}mbients},
journal = {Computer Languages},
year = {2002},
volume = {28},
number = {1},
pages = {61-99},
month = {nov},
}
M. Bugliesi, G. Castagna, and S. Crafa: Reasoning about security in Mobile Ambients. In CONCUR 2001, 12th. International
Conference on Concurrency Theory, n. 2154, LNCS, pag. 102-120, Springer, 2001. Contained in [BCC04]. [Abstract] The paper gives an assessment of security for Mobile
Ambients, with specific focus on mandatory access
control (MAC) policies in multilevel security systems.
The first part of the paper reports on different formalization
attempts for MAC policies in the Ambient Calculus, and provides
an in-depth analysis of the problems one encounters. As it turns
out, MAC security does not appear to have fully convincing
interpretations in the calculus.
The second part proposes a solution to this impasse,
based on a variant of Mobile Ambients. A type system for
resource access control is defined, and the new calculus is
discussed and illustrated with several examples of resource
management policies.[BibTeX] Click for bibtex entry@inproceedings{BCC01b,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Reasoning about security in Mobile Ambients},
booktitle = {{CONCUR} 2001, 12th.\ International
Conference on Concurrency Theory},
year = {2001},
number = {2154},
series = {LNCS},
pages = {102-120},
address = {Aahrus, Danemark},
publisher = {Springer},
note = {Contained in~\cite{BCC04}},
}
J. Vitek and G. Castagna: Mobile Computations and Hostile Hosts. In Journées Francophones des Langages Applicatifs, pag. 113-132, Editions Hermès, 1999. [Abstract] This paper scratches the surface of the problem of
classifying the attacks that a mobile computation can be subjected to
in an open network. The discussion is based on a simplified version
of the Seal Calculus. We show how the impact of these attacks on the
semantics of the calculus and on the notion of observational
equivalence.[BibTeX] Click for bibtex entry@inproceedings{VC99,
author = {J.~Vitek and G. Castagna},
title = {Mobile Computations and Hostile Hosts},
booktitle = {Journ{é}es Francophones des Langages Applicatifs},
year = {1999},
pages = {113-132},
publisher = {Editions Herm{è}s},
}
G. Castagna: Types et Modèles : des langages objets séquentiels à la mobilité et à la sécurité, Université Paris 7, Habilitation à diriger des recherches, January, 2002. [BibTeX]Click for bibtex entry@phdthesis{Cas02hab,
author = {G. Castagna},
title = {Types et {M}od{è}les : des langages objets s{é}quentiels {à} la mobilit{é} et {à} la s{é}curit{é}},
school = {Universit{é} Paris 7},
year = {2002},
type = {Habilitation {à} diriger des recherches},
month = {jan},
}
Object-Oriented Languages
G. Castagna: Object-Oriented Programming: A Unified Foundation, Birkäuser, Progress in Theoretical Computer Science Series, 1997. ISBN 3-7643-3905-5 (hardcover, 388 pages). [BibTeX]Click for bibtex entry@book{oobook,
author = {G. Castagna},
title = {Object-Oriented Programming: A Unified Foundation},
publisher = {Birk{ä}user},
year = {1997},
series = {Progress in Theoretical Computer Science Series},
address = {Boston},
note = {ISBN 3-7643-3905-5 (hardcover, 388 pages)},
}
G. Castagna: Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers). Logical Methods in Computer Science, n. 16, pag. 15:1―15:58, 2020. [Abstract] Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language.
In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue.
Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers.
Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.[BibTeX] Click for bibtex entry@article{Cas15,
author = {G. Castagna},
title = {Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers)},
journal = {Logical Methods in Computer Science},
year = {2020},
number = {16},
pages = {15:1--15:58},
note = {\ifFRENCH\else First version: 2013.\fi},
}
J. Boyland and G. Castagna: Parasitic Methods: Implementation of Multi-Methods for Java. In OOPSLA '97, 12th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, vol. 32(10), pag. 66-76, 1997. [Abstract] In an object-oriented programming language, method selection
is (usually) done at run-time using the class of the receiver.
Some object-oriented languages (such as CLOS) have
multi-methods which comprise several methods selected on
the basis of the run-time classes of all the parameters, not
just the receiver. Multi-methods permit intuitive and type-safe
definition of binary methods such as structural equality, set
inclusion and matrix multiplication, just to name a few. Java
as currently defined does not support multi-methods. This paper
defines a simple extension to Java that enables the writing of
``encapsulated'' multi-methods through the use of
parasitic methods, methods that ``attach'' themselves to
other methods. Encapsulated multi-methods avoid some of the
modularity problems that arise with fully general multi-methods.
Furthermore, this extension yields for free both covariant and
contravariant specialization of methods (besides Java's current
invariant specialization).
Programs using this extension can be translated automatically at
the source level into programs that do not; they are modular,
type-safe, and allow separate compilation.[BibTeX] Click for bibtex entry@inproceedings{BC97,
author = {J. Boyland and G. Castagna},
title = {Parasitic Methods: Implementation of Multi-Methods for {J}ava},
booktitle = {OOPSLA '97, 12th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications},
year = {1997},
volume = {32(10)},
pages = {66-76},
}
G. Castagna and L. Liquori: A typed calculus of objects. In ASIAN '96, 1st Asian Computing Science Conference, n. 1179, LNCS, pag. 129-141, Springer, 1996. [Abstract] In this paper, we present an explicitly typed version of
the Lambda Calculus of Objects of Fisher, Honsell and Mitchell,
which is a development of the object-calculi defined by Bruce
and Longo. This calculus supports object extension in
presence of object subsumption. Extension is the ability
of modify the behavior of an object by adding new methods (and
inheriting the existing ones). Object subsumption allows to use
objects with a bigger interface in a context expecting another
object with a smaller interface. This calculus has a sound and
decidable type system, ``width'' subtyping, and it allows for
first-class method bodies.[BibTeX] Click for bibtex entry@inproceedings{LC96,
author = {G. Castagna and L. Liquori},
title = {A typed calculus of objects},
booktitle = {ASIAN '96, 1st Asian Computing Science Conference},
year = {1996},
editor = {J.~Jaffar and R.~Yap},
number = {1179},
series = {LNCS},
pages = {129-141},
publisher = {Springer},
}
J. Boyland and G. Castagna: Type-safe compilation of covariant specialization: a practical case. In ECOOP '96, 10th European Conference on Object-Oriented Programming, n. 1098, LNCS, pag. 3-25, Springer, 1996. [Abstract] Despite its lack of type safety, some typed object-oriented
languages use covariant specialization for methods. In
this work, we show how one may modify the semantics of languages
that use covariant specialization in order to improve their type
safety. We demonstrate our technique using O_{2}, a strongly
and statically typed object-oriented database programming
language which uses covariant specialization. We propose a
modification to the O_{2} compiler that adds code to correct
previously ill-typed computations that arise from the use of
covariant specialization. The modification we propose does not
affect the semantics of those computations without type errors.
Furthermore, the new semantics of the previously ill-typed
computations is defined in a very ``natural'' way and ensures
the type safety (w.r.t. covariance) of the program.
Since the solution consists of a conservative
backward-compatible modification of the compiler, it does not
require, unlike other solutions, any modification of existing
O_{2} code. Our solution is based solely on a type-theoretic
analysis and thus is general. Therefore, although this paper
applies it to a particular programming language, the same ideas
could easily be applied to other languages that use covariant
specialization.[BibTeX] Click for bibtex entry@inproceedings{Cas96,
author = {J. Boyland and G. Castagna},
title = {Type-safe compilation of covariant specialization: a practical case},
booktitle = {ECOOP '96, 10th European Conference on Object-Oriented Programming},
year = {1996},
editor = {Pierre Cointe},
number = {1098},
series = {LNCS},
pages = {3-25},
publisher = {Springer},
}
K. Bruce, L. Cardelli, G. Castagna and
The Hopkins Object Group, G. Leavens, and B. Pierce: On Binary Methods. Theory and Practice of Object Systems, vol. 1, n. 3, pag. 221-242, 1996. [Abstract] Giving types to binary methods causes significant problems for
object-oriented language designers and programmers. This paper offers
a comprehensive description of the problems arising from typing binary
methods, and collects and contrasts diverse views and solutions.
It summarizes the current debate on the problem of binary
methods for a wide audience.[BibTeX] Click for bibtex entry@article{BruEtAl96,
author = {K. Bruce and L. Cardelli and G. Castagna and
The~Hopkins~Object~Group and G. Leavens and B. Pierce},
title = {On Binary Methods},
journal = {Theory and Practice of Object Systems},
year = {1996},
volume = {1},
number = {3},
pages = {221-242},
}
G. Castagna: Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, vol. 17, n. 3, pag. 431-447, 1995. [Abstract] In type-theoretic research on object-oriented programming, the
issue of ``covariance versus contravariance'' is a topic of continuing
debate. In this short note we argue that covariance and
contravariance appropriately characterize two distinct and independent
mechanisms. The so-called contravariance rule correctly captures the
subtyping relation (that relation which establishes which sets
of functions can replace another given set in every context).
A covariant relation, instead, characterizes the specialization of code (i.e., the definition of new code which
replaces old definitions in some particular cases).
Therefore, covariance and contravariance are not opposing views, but
distinct concepts that each have their place in object-oriented
systems. Both can (and should) be integrated in a type-safe manner in
object-oriented languages.
We also show that the independence of the two mechanisms is not
characteristic of a particular model but is valid in general, since
covariant specialization is present in record-based models, although
it is hidden by a deficiency of all existing calculi that realize this
model.
As an aside, we show that the λ&-calculus can be taken
as the basic calculus for both an overloading-based and a record-based
model. Using this approach, one not only obtains a more uniform vision
of object-oriented type theories, but in the case of the record-based
approach, one also gains multiple dispatching, a feature that existing
record-based models do not capture.[BibTeX] Click for bibtex entry@article{Cas94,
author = {G. Castagna},
title = {Covariance and contravariance: conflict without a cause},
journal = {ACM Transactions on Programming Languages and Systems},
year = {1995},
volume = {17},
number = {3},
pages = {431-447},
}
G. Castagna, G. Ghelli, and G. Longo: A calculus for overloaded functions with subtyping. Information and Computation, vol. 117, n. 1, pag. 115-135, February, 1995. [Abstract] We present a simple extension of typed λ-calculus
where functions can be overloaded by putting different
``branches of code'' together. When the function is applied,
the branch to execute is chosen according to a particular
selection rule which depends on the type of the argument. The
crucial feature of the present approach is that the branch
selection depends on the ``run-time type'' of the argument,
which may differ from its compile-time type, because of the
existence of a subtyping relation among types. Hence overloading
cannot be eliminated by a static analysis of code, but is an
essential feature to be dealt with during computation. We obtain
in this way a type-dependent calculus, which differs from the
various λ-calculi where types do not play any role
during computation. We prove Confluence and a generalized
Subject-Reduction theorem for this calculus. We prove Strong
Normalization for a ``stratified'' subcalculus. The definition
of this calculus is guided by the understanding of
object-oriented features and the connections between our
calculus and object-orientedness are extensively stressed. We
show that this calculus provides a foundation for typed
object-oriented languages which solves some of the problems of
the standard record-based approach.[BibTeX] Click for bibtex entry@article{CGL94,
author = {G. Castagna and G. Ghelli and G. Longo},
title = {A calculus for overloaded functions with subtyping},
journal = {Information and Computation},
year = {1995},
volume = {117},
number = {1},
pages = {115-135},
month = {feb},
}
G. Castagna: A meta-language for typed object-oriented languages. Theoretical Computer Science, vol. 151, n. 2, pag. 297-352, November, 1995. [Abstract] In [CGL94] we defined the λ&-calculus, a
simple extension of the typed λ-calculus to model typed
object-oriented languages. This paper is the continuation or,
rather, the companion of [CGL94] since it analyzes the
practical counterpart of the theoretical issues introduced
there. Indeed, to develop a formal study of type systems for
object-oriented languages we define a meta-language based on
λ& and we show, by a practical example, how it can be
used it to prove properties of a language. To this purpose, we
define a toy object-oriented language and its type-checking
algorithm; then we translate this toy language into our
meta-language. The translation gives the semantics of the toy
language and a theorem on the translation of well-typed programs
proves the correctness of the type-checker of the toy language.
As an aside we also illustrate the expressivity of the
λ&-based model by showing how to translate existing
features like multiple inheritance and multiple dispatch, but
also by integrating in the toy language new features directly
suggested by the model, such as first-class messages, a
generalization of the use of super and the use of explicit
coercions. An important novelty with respect to previous systems
is that we show how to model multiple dispatch also in the
presence of a notion of receiver (i.e. of a privileged
argument to which the message is passed), notion that is absent
in languages like CLOS.[BibTeX] Click for bibtex entry@article{Cas93,
author = {G. Castagna},
title = {A meta-language for typed object-oriented languages},
journal = {Theoretical Computer Science},
year = {1995},
volume = {151},
number = {2},
pages = {297-352},
month = {nov},
}
G. Castagna: A meta-language for typed object-oriented languages. In FST&TCS '93, 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, n. 761, LNCS, pag. 52-71, Springer, December, 1993. Extended abstract of [Cas93]. [Abstract] In [CGL94] we defined the λ&-calculus, a
simple extension of the typed λ-calculus to model typed
object-oriented languages. To develop a formal study of type
systems for object-oriented languages we define, in this paper,
a meta-language based on λ& and we show by a practical
example how to use it to prove properties of a language. To this
purpose we define a toy object-oriented language and its
type-checking algorithm; then we translate this toy language
into our meta-language. The translation gives the semantics of
the toy language and a theorem on the translation of well-typed
programs proves the correction of the type-checker of the toy
language.
As an aside we also illustrate the expressivity of the
λ&-based model by showing how to translate existing
features like multiple inheritance and multiple dispatch, but
also by integrating in the toy language new features directly
suggested by the model, such as first-class messages, a
generalization of the use of super and the use of explicit
coercions.[BibTeX] Click for bibtex entry@inproceedings{Cas93ea,
author = {G. Castagna},
title = {A meta-language for typed object-oriented languages},
booktitle = {{FST\&TCS} '93, 13th Conference on the Foundations of Software Technology and Theoretical Computer Science},
year = {1993},
editor = {R.K. Shyamasundar},
number = {761},
series = {LNCS},
pages = {52-71},
address = {Bombay, India},
month = {dec},
publisher = {Springer},
note = {Extended abstract of~\cite{Cas93}},
}
G. Castagna, G. Ghelli, and G. Longo: A calculus for overloaded functions with subtyping. In ACM Conference on LISP and Functional Programming, pag. 182-192, ACM Press, July, 1992. Extended abstract of [CGL94]. [Abstract] We present a simple extension of typed λ-calculus
where functions can be overloaded by adding different
``pieces of code''. In short, the code of an overloaded function
is formed by several branches of code; the branch to execute is
chosen, when the function is applied, according to a particular
selection rule which depends on the type of the argument. The
crucial feature of the present approach is that a subtyping
relation is defined among types, such that the type of a term
generally decreases during computation, and this fact induces a
distinction between the ``compile-time'' type and the
``run-time'' type of a term. We study the case of overloaded
functions where the branch selection depends on the run-time
type of the argument, so that overloading cannot be eliminated
by a static analysis of code, but is an essential feature to be
dealt with during computation. We obtain in this way a
type-dependent calculus, which differs from the various
λ-calculi where types do not play, essentially, any
rôle during computation. We prove Confluence and Strong
Normalization for this calculus as well as a generalized
Subject-Reduction theorem.
The definition of this calculus is driven by the understanding
of object-oriented features and the connections between our
calculus and object-orientedness are extensively stressed. We
show that this calculus provides a foundation for typed
object-oriented languages which solves some of the problems of
the standard record-based approach. It also provides a
type-discipline for a relevant fragment of the ``core
framework'' of CLOS.[BibTeX] Click for bibtex entry@conference{CGL92,
author = {G. Castagna and G. Ghelli and G. Longo},
title = {A calculus for overloaded functions with subtyping},
booktitle = {ACM Conference on LISP and Functional Programming},
year = {1992},
pages = {182-192},
address = {San Francisco},
month = {jul},
publisher = {ACM Press},
note = {Extended abstract of~\cite{CGL94}},
}