Giuseppe CastagnaSenior Researcher
CNRS
Paris Diderot University
PPS Laboratory
Tel : +33 1 5727 9340
Fax: +33 1 5727 9297
V-card:
Geolocation:
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
- Publications by type: non exhaustive list containing at least the main references
- Publications by topic: the same publications ordered by their topic
- Latest papers: a selection of most recent and possibly unpublished work
- Selected papers: some papers I am proud of.
Some Links
- The ℂDuce
project: a language for type-safe and fast query and transformation of XML documents - Typex Typeful and certified XML (ANR Project)
- BETTY Behavioural Types for Reliable Large-Scale Software Systems (ICT COST Action)
- Codex Efficiency, Dynamicity and Composition for XML: Models, Algorithms and Systems (ANR Project)
- ESOP (Steering Commitee Chair)
- ETAPS (Steering Committee & Executive Board)
- OOPSLA 2013 (PC member)
- ECOOP 2013 (Program Committee Chair)
- ITRS 2012 (Invited speaker)
- MFCS 2012 (PC member)
- FLOPS 2012 (PC member)
- FMOODS & FORTE 2011 (Invited speaker)(paper) (slides)
- OOPSLA 2011 (PC member)
- ESOP 2010 (PC member)
- ITRS 2010 (PC member)
- ESOP 2009 (Program Committee Chair)
- PLAN-X 2009 (PC member)
- SBLP 2007 (Invited speaker) (slides)
- ICALP /PPDP 2005 (Joint keynote speaker) (paper) (slides)
- DBPL /XSYM 2005 (Joint Invited speaker) (paper) (slides)
- ICTCS 2005 (Invited speaker) (paper)
Latest Papers (October 2012)
: A Core Calculus for XQuery 3.0, April, 2013.
[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 I. Hyeonseung and K. Nguyễn and V. Benzaken}, title = {A Core Calculus for {XQuery} 3.0}, note = {}, month = {apr}, year = {2013}, }
[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 I. Hyeonseung and K. Nguyễn and V. Benzaken}, title = {A Core Calculus for {XQuery} 3.0}, note = {}, month = {apr}, year = {2013}, }
: Polymorphic Functions with Set-Theoretic Types, December, 2012.
[Abstract] We present a type system and local type inference for a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). This work provides the theoretical foundations and technical machinery needed to start the design and implementation of polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@unpublished{CNXL12, author = {G. Castagna and K. Nguyễn and Z. Xu and S. Lenglet}, title = {Polymorphic Functions with Set-Theoretic Types}, note = {}, month = {dec}, year = {2012}, }[Extended Version]
[Abstract] We present a type system and local type inference for a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). This work provides the theoretical foundations and technical machinery needed to start the design and implementation of polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@unpublished{CNXL12, author = {G. Castagna and K. Nguyễn and Z. Xu and S. Lenglet}, title = {Polymorphic Functions with Set-Theoretic Types}, note = {}, month = {dec}, year = {2012}, }[Extended Version]
: 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}, }
[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}, }
: 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]
[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]
: Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems, vol. 38, n. 1, pag. , 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 = {}, }
[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 = {}, }
: 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}, }
[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}, }
: Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, September, 2011. Type-checker prototype available at http://www.pps.univ-paris-diderot.fr/~zhiwu/files/subtype-checker-0.3.tar.gz.
[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}, note = {Type-checker prototype available at \url{http://www.pps.univ-paris-diderot.fr/~zhiwu/files/subtype-checker-0.3.tar.gz}}, }[Extended Version]
[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}, note = {Type-checker prototype available at \url{http://www.pps.univ-paris-diderot.fr/~zhiwu/files/subtype-checker-0.3.tar.gz}}, }[Extended Version]
: 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 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]
[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]
: 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}, }
[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}, }
|
|
