Giuseppe Castagna's Home Page
Current Interests

Programming languages, models of computation, language level security, mobility, type theory, object-oriented programming, process algebras, languages for XML, web-services.

Honors and awards

Member peer elected at the Academia Europæa, section B2: INFORMATICS.

CACM Research Highlights nomination by ACM SIGPLAN for the article “Set-Theoretic Foundation of Parametric Polymorphism and Subtyping"

Publications
Recent Professional Service
Some Links
Latest Papers (May 2017)
G. Castagna: Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers), 2015. Unpublished manuscript.new
[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.[BibTeX] Click for bibtex entry@misc{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)}, year = {2015}, note = {Unpublished manuscript}, }
G. Castagna and V. Lanvin: Gradual Typing with Union and Intersection Types. In ICFP '17, 22nd ACM SIGPLAN International Conference on Functional Programming, pag. , September, 2017.new
[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@inproceedings{CL16, author = {G. Castagna and V. Lanvin}, title = {Gradual Typing with Union and Intersection Types}, booktitle = {ICFP\,'17, 22nd ACM SIGPLAN International Conference on Functional Programming}, year = {2017}, pages = {}, month = {sep}, }
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.new
[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}, }
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, 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]
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.
[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}, }
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}, }