Page Web de Giuseppe Castagna
Intérêts actuels

Langages de programmation, modèles d'execution, sécurité, mobilité, théorie des types, programmation orientée à objets, algèbres de processus, langages pour XML, services web.

Prix et distinctions

Membre elu à l'Academia Europæa, section B2: Informatique.

CACM Research Highlights nomination par ACM SIGPLAN pour l'article “Set-Theoretic Foundation of Parametric Polymorphism and Subtyping"

Publications
Quelques Liens
Derniers travaux (novembre 2013)
G. Castagna, H. Im, K. Nguyễn et V. Benzaken : A Core Calculus for XQuery 3.0, avril, 2013. Unpublished manuscript.new
[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@unpublished{CHNB13, author = {G. Castagna and H. Im and K. Nguyễn and V. Benzaken}, title = {A Core Calculus for {XQuery} 3.0}, note = {Unpublished manuscript}, month = {apr}, year = {2013}, }
G. Castagna, K. Nguyễn, Z. Xu et P. Abate : Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction, novembre, 2013. Unpublished manuscript.new
[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@unpublished{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}, note = {Unpublished manuscript}, month = {nov}, year = {2013}, }
G. Castagna : A Handbook for [ECOOP] PC Chairs, 2013. Included in the preface of the proceedings of ECOOP 2013, the 27th European Conference on Object-Oriented Programming, LNCS n. 9720, Springer.new
[Abstract] These notes describe how I organized the selection process for ECOOP. In particular they contain a list of tasks that are responsibility of the Program Committee (PC) chair before, during, and after the selection, as well as a description of the six-phases organization I used for selection.[BibTeX] Click for bibtex entry@misc{Cas13, author = {G. Castagna}, title = {A Handbook for [{ECOOP}] {PC} {C}hairs}, year = {2013}, note = {Included in the preface of the proceedings of ECOOP 2013, the 27th European Conference on Object-Oriented Programming, LNCS n.\ 9720, Springer}, }
G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet et L. Padovani : Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. Dans POPL '14, 41th ACM Symposium on Principles of Programming Languages, janvier, 2014. To appear.new
[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, 41th ACM Symposium on Principles of Programming Languages}, year = {2014}, month = {jan}, note = {To appear}, }
V. Benzaken, G. Castagna, K. Nguyễn et J. Siméon : Static and Dynamic Semantics of NoSQL Languages. Dans POPL '13, 40th ACM Symposium on Principles of Programming Languages, pag. 101―113, 2013.new
[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 et 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.new
[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 et 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 et Z. Xu : Set-theoretic Foundation of Parametric Polymorphism and Subtyping. Dans ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, septembre, 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 et L. Padovani : On Global Types and Multi-Party Sessions. Dans FMOODS & FORTE 2011, joint 13th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems and 31th 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 31th {IFIP} International Conference on FORmal TEchniques for Networked and Distributed Systems.}, year = {2011}, number = {6722}, series = {LNCS}, publisher = {Springer}, note = {Invited talk}, }[Extended Version]
V. Benzaken, G. Castagna, H. Hosoya, B.C. Pierce et 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}, }