Giuseppe CastagnaDirecteur de Recherche
CNRS
Université Paris 7
Laboratoire PPS
Tél : +33 1 4427 8138
Fax: +33 1 4427 8654
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.
Publications
- Publications par genre : liste non exahustive contenant au moins les travaux principaux
- Publications par sujet : les mêmes publications ordonnées par sujet
- Derniers travaux recents : une selection de travaux recents pas forcement publiés
- Publications choisies : morceaux choisis.
Quelques Liens
- 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)
- ESOP 2010 (PC member)
- ITRS 2010 (PC member)
- ESOP 2009 (Programme Chair)
- PLAN-X 2009 (PC member)
- ICALP 2008 (PC member)
- PLAN-X 2008 (Steering Commitee)
- Longo Symposium (Co-organizer)
- SBLP 2007 (Invited speaker) (slides)
- ESOP 2007 (PC member)
- PLAN-X 2007 (Steering Commitee)
- ESOP 2006 (PC member)
- POPL 2006 (PC member)
- PLAN-X 2006 (Programme Chair)
- ICALP /PPDP 2005 (Joint keynote speaker) (paper) (slides)
- DBPL /XSYM 2005 (Joint Invited speaker) (paper) (slides)
- ICTCS 2005 (Invited speaker) (paper)
Derniers travaux (septembre 2009)
: 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. (19:1―19:61), 2009. Supersedes the article in POPL '08.
[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 = {(19:1--19:61)}, note = {Supersedes the article in POPL '08}, }
[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 = {(19:1--19:61)}, note = {Supersedes the article in POPL '08}, }
: Contracts for Mobile Processes. Dans 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}, }
: Foundations of Session Types. Dans 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}, }
: Typed Iterators for XML. Dans ICFP '08: 13th ACM-SIGPLAN International Conference on Functional Programming, pag. 15―26, avril, 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. Nguyen}, title = {Typed Iterators for {XML}}, booktitle = {ICFP '08: 13th {ACM-SIGPLAN} International Conference on Functional Programming}, year = {2008}, pages = {15--26}, month = {apr}, }
[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. Nguyen}, title = {Typed Iterators for {XML}}, booktitle = {ICFP '08: 13th {ACM-SIGPLAN} International Conference on Functional Programming}, year = {2008}, pages = {15--26}, month = {apr}, }
: 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 Inclue, \'etend les articles de LICS '02 et ICALP/PPDP '05 \else Extends and supersedes LICS '02 and ICALP/PPDP '05 articles\fi}, }
[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 Inclue, \'etend les articles de LICS '02 et ICALP/PPDP '05 \else Extends and supersedes LICS '02 and ICALP/PPDP '05 articles\fi}, }
: 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}, }
[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}, }
|
|
