Giuseppe CastagnaSenior Researcher
CNRS
Paris 7 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.
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 CDuce
project: a language for type-safe and fast query and transformation of XML documents - CODEX Efficiency, Dynamicity and Composition for XML: Models, Algorithms and Systems (ANR Project)
- ETAPS (Steering Commitee & Executive Board)
- ITRS 2012 (Invited speaker)
- 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 (Programme 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 (November 2011)
: The next 700 NoSQL languages, November, 2011. Soumis à une conférence internationale.
[Abstract] We present a calculus for processing semistructured data that spans differences of application area among several novel query languages, 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 information that is both precise, and flexible enough to handle structured and semistructured data. We illustrate the use of that calculus by encoding a large fragment of Jaql, including operations and iterators over JSON, embedded SQL expressions, and co-grouping.[BibTeX] Click for bibtex entry@unpublished{BCNS12, author = {V. Benzaken and G. Castagna and K. Nguyễn and J. Siméon}, title = {The next 700 {NoSQL} languages}, note = {Soumis à une conférence internationale}, month = {nov}, year = {2011}, }
[Abstract] We present a calculus for processing semistructured data that spans differences of application area among several novel query languages, 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 information that is both precise, and flexible enough to handle structured and semistructured data. We illustrate the use of that calculus by encoding a large fragment of Jaql, including operations and iterators over JSON, embedded SQL expressions, and co-grouping.[BibTeX] Click for bibtex entry@unpublished{BCNS12, author = {V. Benzaken and G. Castagna and K. Nguyễn and J. Siméon}, title = {The next 700 {NoSQL} languages}, note = {Soumis à une conférence internationale}, month = {nov}, year = {2011}, }
: On Global Types and Multi-Party Sessions. Logical Methods in Computer Science, 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}, note = {\ifFRENCH Version étendue de~\cite{CDP11}. À paraître\else Extended version of the invited talk given at FMOODS \& FORTE 2011, to appear\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}, note = {\ifFRENCH Version étendue de~\cite{CDP11}. À paraître\else Extended version of the invited talk given at FMOODS \& FORTE 2011, to appear\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.jussieu.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.jussieu.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.jussieu.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]
: 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}, }
[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}, }
: 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}, }
[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}, }
: 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}, }
[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}, }
: 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]
[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]
: 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}, }
|
|
