Giuseppe Castagna: Publications par sujet

Publications par sujet

Cette page contient la plupart de mes publications ordonées par argument (la même publication pouvant apparaître sous plusieurs arguments). La liste complète se trouve ici. Ces mêmes publications ordonnées par genre sont disponibles à cette page.

Liste des Sujets :

[ Page générée automatiquement le vendredi, 12 juillet 2024 des fichiers suivants : /home/beppe/BIBLIO/castagna-unp.bib /home/beppe/BIBLIO/castagna.bib ]

Théorie de types et sous-typage

Giuseppe Castagna et Guillaume Duboc : Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir, 7, 2024. Submitted.
[Abstract] We define several techniques to extend gradual typing with semantic subtyping, specifically targeting dynamic languages. Focusing on the Elixir programming language, we provide the theoretical foundations for its type system. Our approach demonstrates how to achieve type soundness for gradual typing in existing dynamic languages without modifying their compilation, while still maintaining high precision. This is accomplished through the static detection of strong functions, which leverage runtime checks inserted by the programmer or performed by the virtual machine, and through a fine-grained type analysis of pattern-matching expressions with guards.[BibTeX] @unpublished{CD25, author = {Giuseppe Castagna and Guillaume Duboc}, title = {Guard Analysis and Safe Erasure Gradual Typing: a Type System for {Elixir}}, note = {Submitted}, month = {7}, year = {2024}, }

Giuseppe Castagna et Loïc Peyrot : Polymorphic Records for Dynamic Languages, 4, 2024. ArXiv preprint: arXiv:2404.00338.
[Abstract] We define and study row polymorphism for a type system with set-theoretic types, specifically union, intersection, and negation types. We consider record types that embed row variables and define a subtyping relation by interpreting types into sets of record values and by defining subtyping as the containment of interpretations. We define a functional calculus equipped with operations for field extension, selection, and deletion, its operational semantics, and a type system that we prove to be sound. We provide algorithms for deciding the typing and subtyping relations. This research is motivated by the current trend of defining static type system for dynamic languages and, in our case, by an ongoing effort of endowing the Elixir programming language with a gradual type system.[BibTeX] @unpublished{CP24, author = {Giuseppe Castagna and Loïc Peyrot}, title = {Polymorphic Records for Dynamic Languages}, note = {ArXiv preprint: \href{https://arxiv.org/abs/2404.00338}{arXiv:2404.00338}}, month = {4}, year = {2024}, }

G. Castagna : Object-Oriented Programming: A Unified Foundation, Birkäuser, Progress in Theoretical Computer Science Series, 1997. ISBN 3-7643-3905-5 (hardcover, 388 pages).
[BibTeX]@book{oobook, author = {G. Castagna}, title = {Object-Oriented Programming: A Unified Foundation}, publisher = {Birk{ä}user}, year = {1997}, series = {Progress in Theoretical Computer Science Series}, address = {Boston}, note = {ISBN 3-7643-3905-5 (hardcover, 388 pages)}, }

Giuseppe Castagna : Programming with Union, Intersection, and Negation Types. Dans The French School of Programming, Springer, pag. 309―378, mars, 2024. ISBN 978-3-031-34517-3. Preprint at arXiv:2111.03354.
[Abstract] In this essay I present the advantages and, I dare say, the beauty of programming in a language with set-theoretic types, that is, types that include union, intersection, and negation type connectives. I show by several examples how set-theoretic types are necessary to type some common programming patterns, but also how they play a key role in typing several language constructs―from branching and pattern matching to function overloading and type-cases―very precisely. I start by presenting the theory of types known as semantic subtyping and extend it to include polymorphic types. Next, I discuss the design of languages that use these types. I start by defining a theoretical framework that covers all the examples given in the first part of the presentation. Since the system of the framework cannot be effectively implemented, I then describe three effective restrictions of this system: (i) a polymorphic language with explicitly-typed functions, (ii) an implicitly typed polymorphic language à la Hindley-Milner, and (iii) a monomorphic language that, by implementing classic union-elimination, precisely reconstructs intersection types for functions and implements a very general form of occurrence typing. I conclude the presentation with a short overview of other aspects of these languages, such as pattern matching, gradual typing, and denotational semantics.[BibTeX] @incollection{Cas24, author = {Giuseppe Castagna}, title = {Programming with Union, Intersection, and Negation Types}, booktitle = {The French School of Programming}, publisher = {Springer}, year = {2024}, editor = {Bertrand Meyer}, pages = {309--378}, month = {mar}, note = {ISBN 978-3-031-34517-3. Preprint at \href{https://arxiv.org/abs/2111.03354}{arXiv:2111.03354}}, }

Giuseppe Castagna, Guillaume Duboc et José Valim : The Design Principles of the Elixir Type System. The Art, Science, and Engineering of Programming, vol. 8, n° 2, 2024. Video of the presentation I gave at the Erlang Symposium 2023: https://youtu.be/VYmo867YF6g. Also available, Guillaume Duboc's presentation at ElixirConf EU 2023: https://www.youtube.com/watch?v=gJJH7a2J9O8.
[Abstract] Elixir is a dynamically-typed functional language running on the Erlang Virtual Machine, designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers. Static typing seems nowadays to be the most important request coming from the Elixir community. We present a gradual type system we plan to include in the Elixir compiler, outline its characteristics and design principles, and show by some short examples how to use it in practice. Developing a static type system suitable for Erlang's family of languages has been an open research problem for almost two decades. Our system transposes to this family of languages a polymorphic type system with set-theoretic types and semantic subtyping. To do that, we had to improve and extend both semantic subtyping and the typing techniques thereof, to account for several characteristics of these languages―and of Elixir in particular―such as the arity of functions, the use of guards, a uniform treatment of records and dictionaries, the need for a new sound gradual typing discipline that does not rely on the insertion at compile time of specific run-time type-tests but, rather, takes into account both the type tests performed by the virtual machine and those explicitly added by the programmer. The system presented here is ``gradually'' being implemented and integrated in Elixir, but a prototype implementation is already available. The aim of this work is to serve as a longstanding reference that will be used to introduce types to Elixir programmers, as well as to hint at some future directions and possible evolutions of the Elixir language.[BibTeX] @article{CDV23, author = {Giuseppe Castagna and Guillaume Duboc and José Valim}, title = {The Design Principles of the {Elixir} Type System}, journal = {The Art, Science, and Engineering of Programming}, year = {2024}, volume = {8}, number = {2}, note = {Video of the presentation I gave at the Erlang Symposium 2023: \url{https://youtu.be/VYmo867YF6g}. Also available, Guillaume Duboc's presentation at ElixirConf EU 2023: \url{https://www.youtube.com/watch?v=gJJH7a2J9O8}}, }

Giuseppe Castagna, Mickaël Laurent et Kim Nguyễn : Polymorphic Type Inference for Dynamic Languages. Proc. ACM Program. Lang., vol. 8, n° POPL, janvier, 2024.
[Abstract] We present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that is sound and terminating. This yields a system in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can express the overloaded behavior of the functions they type (thanks to the intersection introduction rule) and that are deduced by applying advanced techniques of type narrowing (thanks to the union elimination rule). This makes the system a prime candidate to type dynamic languages.[BibTeX] @article{CLN24, author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn}, title = {Polymorphic Type Inference for Dynamic Languages}, journal = {Proc. ACM Program. Lang.}, year = {2024}, volume = {8}, number = {POPL}, month = {jan}, }

Giuseppe Castagna : Typing Records, Maps, and Structs. Proc. ACM Program. Lang., vol. 7, n° ICFP, septembre, 2023. The video of the presentation given at ICFP 23 is available here.
[Slides] [Abstract] Records are finite functions from keys to values. In this work we focus on two main distinct usages of records: structs and maps. The former associate different keys to values of different types, they are accessed by providing nominal keys, and trying to access a non-existent key yields an error. The latter associate all keys to values of the same type, they are accessed by providing expressions that compute a key, and trying to access a non-existent key usually yields some default value such as "Null" or "nil". Here, we propose a type theory that covers both kinds of usage, where record types may associate to different types either single keys (as for structs) or sets of keys (as for maps) and where the same record expression can be accessed and used both in the struct-like style and in the map-like style we just described. Since we target dynamically-typed languages our type theory includes union and intersection types, characterized by a subtyping relation. We define the subtyping relation for our record types via a semantic interpretation and derive the decomposition rules to decide it, define a backtracking-free subtyping algorithm that we prove to be correct, and provide a canonical representation for record types that is used to define various type operators needed to type record operations such as selection, concatenation, and field deletion.[BibTeX] @article{Cas23, author = {Giuseppe Castagna}, title = {Typing Records, Maps, and Structs}, journal = {Proc. ACM Program. Lang.}, year = {2023}, volume = {7}, number = {ICFP}, month = {sep}, note = {The video of the presentation given at ICFP 23 is available \href{https://www.irif.fr/\~gc/videos/ICFP23-records.webm}{here}}, }

Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn et Matthew Lutze : On Type-Cases, Union Elimination, and Occurrence Typing. Proc. ACM Program. Lang., vol. 6, n° POPL, janvier, 2022.
[Abstract] We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses "occurrence typing". The latter is a typing technique that takes into account the result of type tests to assign different types to a same expression when it occurs in different branchings of the test. To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.[BibTeX] @article{CLNL22, author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn and Matthew Lutze}, title = {On Type-Cases, Union Elimination, and Occurrence Typing}, journal = {Proc. ACM Program. Lang.}, year = {2022}, volume = {6}, number = {POPL}, month = {jan}, }

Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn et Matthew Lutze : Prototype for Article: On Type-Cases, Union Elimination, and Occurrence Typing, 2022. Online interactive version available at https://typecaseunion.github.io. Reference Article: https://doi.org/10.1145/3498674. Software: https://doi.org/10.1145/3462306.
[BibTeX]@manual{typecaseunion22, author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn and Matthew Lutze}, title = {Prototype for Article: On Type-Cases, Union Elimination, and Occurrence Typing}, year = {2022}, note = {Online interactive version available at \url{https://typecaseunion.github.io}. Reference Article: \url{https://doi.org/10.1145/3498674}. Software: \url{https://doi.org/10.1145/3462306}}, }

G. Castagna, M. Laurent, V. Lanvin et K. Nguyễn : Revisiting Occurrence Typing. Science of Computer Programming, vol. 217, pag. 102781, mars, 2022.
[Abstract] We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types―union types, in particular―it never fully exploited the capabilities of these types. Here we show how, by using set-theoretic types, it is possible to develop a general typing framemork that encompasses and generalizes several aspects of current occurrence typing proposals and that can be applied to tackle other problems such as the inference of intersection types for functions and the optimization of the compilation of gradually typed languages.[BibTeX] @article{CLLN19, author = {G. Castagna and M. Laurent and V. Lanvin and K. Nguyễn}, title = {Revisiting Occurrence Typing}, journal = {Science of Computer Programming}, year = {2022}, volume = {217}, pages = {102781}, month = {mar}, }

G. Castagna : Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers). Logical Methods in Computer Science, vol. 16, n° 1, pag. 15:1―15:58, 2020. First version: 2013. New corrected and enhanced version: February 1, 2023.
[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. Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.[BibTeX] @article{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)}, journal = {Logical Methods in Computer Science}, year = {2020}, volume = {16}, number = {1}, pages = {15:1--15:58}, note = {\ifFRENCH\else First version: 2013. New corrected and enhanced version: February~1, 2023\fi}, }

Giuseppe Castagna, Mariangola Dezani-Ciancaglini, Elena Giachino et Luca Padovani : Foundations of Session Types: 10 Years Later. Dans Principles and Practice of Programming Languages 2019 (PPDP ’19), pag. 1-3, ACM, New York, 2019. Invited talk, Most Influential Paper 10-Years Award.
[BibTeX]@inproceedings{CDGP19, author = {Giuseppe Castagna and Mariangola Dezani-Ciancaglini and Elena Giachino and Luca Padovani}, title = {Foundations of Session Types: 10 Years Later}, booktitle = {Principles and Practice of Programming Languages 2019 (PPDP ’19)}, year = {2019}, pages = {1-3}, publisher = {ACM, New York}, note = {Invited talk, \textit{Most Influential Paper 10-Years Award}}, }

G. Castagna, G. Duboc, V. Lanvin et J. G. Siek : A space-efficient call-by-value virtual machine for gradual set-theoretic types. Dans IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages, septembre, 2019.
[Abstract] We describe the design and implementation of a virtual machine for programming languages that use gradual typing with set-theoretic types focusing on practical issues such as runtime space efficiency, and efficient implementation of tail recursive calls.[BibTeX] @inproceedings{CDLS19, author = {G. Castagna and G. Duboc and V. Lanvin and J. G. Siek}, title = {A space-efficient call-by-value virtual machine for gradual set-theoretic types}, booktitle = {IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages}, year = {2019}, month = {sep}, }

Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani et Jeremy G. Siek : Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, Article 16, n° POPL '19: 46th ACM Symposium on Principles of Programming Languages, janvier, 2019.
[Abstract] We define a new, more semantic interpretation of gradual types and use it to "gradualize" two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define two preorders on types, subtyping and materialization, and we employ these preorders to define three gradual type systems ―Hindley-Milner, with subtyping, and with union and intersection types― which we present in two different forms: declaratively and algorithmically. The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the existing standard rules of the type system. This yields clearer, more intelligible, and streamlined definitions; it also shows a direct correlation between cast insertion and materialization that suggests a logical interpretation of the cast calculus, an essential component of gradual typing systems. For the algorithmic presentation, we show how it can be defined by using already existing constraint solving algorithms simply by adding some pre-/post-processing steps. We relate corresponding declarative and algorithmic presentations by soundness and completeness results. As customary, the semantics of the various gradually-typed languages is given in terms of a compilation into cast calculi that use blame labels to pinpoint cast failures. To that end, we show how to define the operational semantics for casts in the presence of unions and intersections, which is an important and far-from-obvious result. We also show a direct correlation between the safety of a cast and the "polarity" of its blame label, allowing for a simpler formulation of the so-called blame safety property.[BibTeX] @article{CLPS19, author = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G.~Siek}, title = {Gradual Typing: a New Perspective}, journal = {Proc. ACM Program. Lang.}, year = {2019}, volume = {3, Article 16}, number = {POPL\,'19: 46th ACM Symposium on Principles of Programming Languages}, month = {jan}, }

Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona et Elena Zucca : Semantic subtyping for non-strict languages. Dans 24th International Conference on Types for Proofs and Programs (TYPES 2018), vol. 130, Leibniz International Proceedings in Informatics (LIPIcs), pag. 4:1―4:24, Schloss Dagstuhl―Leibniz-Zentrum fuer Informatik, 2019.
[Abstract] Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.[BibTeX] @inproceedings{types18post, author = {Tommaso Petrucciani and Giuseppe Castagna and Davide Ancona and Elena Zucca}, title = {Semantic subtyping for non-strict languages}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, year = {2019}, volume = {130}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, pages = {4:1--4:24}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, }

G. Castagna et V. Lanvin : Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang., vol. 1, Article 41, n° ICFP '17, septembre, 2017.
[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] @article{CL17, author = {G. Castagna and V. Lanvin}, title = {Gradual Typing with Union and Intersection Types}, journal = {Proc. ACM Program. Lang.}, year = {2017}, volume = {1, Article 41}, number = {ICFP\,'17}, 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 et N. Yoshida : Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, vol. 3, pag. 95-230, 2016.
[BibTeX]@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, T. Petrucciani et K. Nguyễn : Set-Theoretic Types for Polymorphic Variants. Dans ICFP '16, 21st ACM SIGPLAN International Conference on Functional Programming, pag. 378-391, septembre, 2016.
[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] @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}, }

G. Castagna, H. Im, K. Nguyễn et V. Benzaken : A Core Calculus for XQuery 3.0. Dans 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] @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 et P. Abate : Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. Dans POPL '15, 42nd ACM Symposium on Principles of Programming Languages, pag. 289―302, janvier, 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] @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 et L. Padovani : Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. Dans POPL '14, 41st ACM Symposium on Principles of Programming Languages, pag. 5―17, janvier, 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] @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 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.
[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] @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.
[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] @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. Extended version of the invited talk given at FMOODS & FORTE 2011.
[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] @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] @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 31st 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] @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 31st {IFIP} International Conference on FORmal TEchniques for Networked and Distributed Systems.}, year = {2011}, number = {6722}, series = {LNCS}, publisher = {Springer}, note = {Invited talk}, }[Extended Version]

G. Castagna et L. Padovani : 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] @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}, }

H. Hosoya, A. Frisch et G. Castagna : 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] @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}, }

G. Castagna, N. Gesbert et L. Padovani : A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems, vol. 31, n° 5, pag. 1―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] @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}, }

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]@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}, }

G. Castagna et K. Nguyễn : 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] @inproceedings{CN08icfp, author = {G. Castagna and K. Nguyễn}, title = {Typed Iterators for {XML}}, booktitle = {ICFP '08: 13th {ACM-SIGPLAN} International Conference on Functional Programming}, year = {2008}, pages = {15--26}, month = {apr}, }

A. Frisch, G. Castagna et V. Benzaken : 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] @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}, }

G. Castagna, N. Gesbert et L. Padovani : A Theory of Contracts for Web Services. Dans POPL '08, 35th ACM Symposium on Principles of Programming Languages, pag. 261―272, janvier, 2008.
[Abstract] Contracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises 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 definition of filters, which are explicit coercions that prevent some possible behaviours of services and, in doing so, they 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 axiomatisation 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 also outline the possible practical impact of such a work and the perspectives of future research it opens.[BibTeX] @inproceedings{CGP08, author = {G. Castagna and N. Gesbert and L. Padovani}, title = {A Theory of Contracts for Web Services}, booktitle = {POPL~'08, 35th ACM Symposium on Principles of Programming Languages}, year = {2008}, pages = {261--272}, month = {jan}, }[Extended Version]

G. Castagna, R. De Nicola et D. Varacca : 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] @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}, }

G. Castagna, M. Dezani-Ciancaglini et D. Varacca : Encoding ℂDuce into the ℂPi-calculus. Dans CONCUR 2006, 17th. International Conference on Concurrency Theory, n° 4137, LNCS, pag. 310-326, Springer, 2006.
[Abstract] CDuce is a functional programming language featuring overloaded functions and a rich type system with recursive types, subtyping, union, negation and intersection types. The boolean constructors have a set-theoretic behaviour defined via a semantic interpretation of the types. The Cpi-calculus is an extension of the pi-calculus that enriches Pierce and Sangiorgi pi-calculus subtyping with union, intersection, and negation types. It is based on the same set-theoretic interpretation as CDuce. In this work we present a type faithful encoding of the CDuce into the Cpi-calculus. This encoding is a modification of the Milner-Turner encoding of the lambda-calculus with subtyping into the pi-calculus with subtyping. The main difficulty to overcome was to find an encoding of the types that respects the subtyping relation. Besides the technical challenge, this effort is interesting because it sheds new light on the Milner-Turner encoding and on the relations between sequential and remote execution of functions/services, in particular in the presence of type-driven semantics. It also confirms the validity of the equational laws for union and intersection types in pi-calculus.[BibTeX] @inproceedings{CDV06, author = {G. Castagna and M. Dezani-Ciancaglini and D. Varacca}, title = {Encoding \cduce{} into the \cpi-calculus}, booktitle = {{CONCUR} 2006, 17th.\ International Conference on Concurrency Theory}, year = {2006}, number = {4137}, series = {LNCS}, pages = {310-326}, publisher = {Springer}, }

G. Castagna : Semantic subtyping: challenges, perspectives, and open problems. Dans ICTCS 2005, Italian Conference on Theoretical Computer Science, n° 3701, Lecture Notes in Computer Science, pag. 1―20, Springer, 2005.
[Slides] [Abstract] Semantic subtyping is a relatively new approach to define subtyping relations where types are interpreted as sets and union, intersection and negation types have the corresponding set-theoretic interpretation. In this lecture we outline the approach, give an aperçu of its expressiveness and generality by applying it to the λ-calculus with recursive and product types and to the π-calculus. We then discuss in detail the new challenges and research perspectives that the approach brings forth.[BibTeX] @inproceedings{Cas05b, author = {G. Castagna}, title = {Semantic subtyping: challenges, perspectives, and open problems}, booktitle = {ICTCS 2005, Italian Conference on Theoretical Computer Science}, year = {2005}, number = {3701}, series = {Lecture Notes in Computer Science}, pages = {1--20}, publisher = {Springer}, }

G. Castagna et A. Frisch : A gentle introduction to semantic subtyping. Dans Proceedings of PPDP '05, the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pages 198-208, ACM Press (full version) and ICALP '05, 32nd International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science n. 3580, pages 30-34, Springer (summary), juillet, 2005. Joint ICALP-PPDP keynote talk.
[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. In this work we show step by step how to define a subtyping relation semantically in the presence of functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm. It also provides a recipe to add set-theoretic union, intersection, and negation types to your favourite language. The presentation is voluntarily kept informal and discursive and the technical details are reduced to a minimum since we rather insist on the motivations, the intuition, and the guidelines to apply the approach.[BibTeX] @inproceedings{CF05, author = {G. Castagna and A. Frisch}, title = {A gentle introduction to semantic subtyping}, booktitle = {\emph{Proceedings of} PPDP '05, the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, \emph{pages 198-208, ACM Press (full version) and} ICALP '05, 32nd International Colloquium on Automata, Languages and Programming, \emph{Lecture Notes in Computer Science n.\ 3580, pages 30-34, Springer (summary)}}, year = {2005}, address = {Lisboa, Portugal}, month = {jul}, note = {Joint ICALP-PPDP keynote talk}, }

G. Castagna, R. De Nicola et D. Varacca : Semantic subtyping for the π-calculus. Dans LICS '05, 20th Annual IEEE Symposium on Logic in Computer Science, pag. , IEEE Computer Society Press, 2005.
[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 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] @inproceedings{CDV05, author = {G. Castagna and R. De~Nicola and D. Varacca}, title = {Semantic subtyping for the $\pi$-calculus}, booktitle = {LICS '05, 20th Annual IEEE Symposium on Logic in Computer Science}, year = {2005}, pages = {}, publisher = {IEEE Computer Society Press}, }

H. Hosoya, A. Frisch et G. Castagna : Parametric Polymorphism for XML. Dans POPL '05, 32nd ACM Symposium on Principles of Programming Languages, pag. 50-62, ACM Press, 2005.
[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] @inproceedings{HFC05, author = {H. Hosoya and A. Frisch and G. Castagna}, title = {Parametric Polymorphism for {XML}}, booktitle = {POPL~'05, 32nd ACM Symposium on Principles of Programming Languages}, year = {2005}, pages = {50-62}, publisher = {ACM Press}, }

A. Frisch, G. Castagna et V. Benzaken : Semantic Subtyping. Dans LICS '02, 17th Annual IEEE Symposium on Logic in Computer Science, pag. 137―146, IEEE Computer Society Press, 2002.
[Abstract] Usually subtyping relations are defined either syntactically by a formal system or semantically by an interpretation of types in an untyped denotational model. In this work we show how to define a subtyping relation semantically, for a language whose operational semantics is driven by types; we consider a rich type algebra, with product, arrow, recursive, intersection, union and complement types. Our approach is to ``bootstrap'' the subtyping relation through a notion of set-theoretic model of the type algebra. The advantages of the semantic approach are manifold. Foremost we get ``for free'' many properties (e.g., the transitivity of subtyping) that, with axiomatized subtyping, would require tedious and error prone proofs. Equally important is that the semantic approach allows one to derive complete algorithms for the subtyping relation or the propagation of types through patterns. As the subtyping relation has a natural (inasmuch as semantic) interpretation, the type system can give informative error messages when static type-checking fails. Last but not least the approach has an immediate impact in the definition and the implementation of languages manipulating XML documents, as this was our original motivation.[BibTeX] @inproceedings{FCB02, author = {A. Frisch and G. Castagna and V. Benzaken}, title = {Semantic {S}ubtyping}, booktitle = {LICS '02, 17th Annual IEEE Symposium on Logic in Computer Science}, year = {2002}, pages = {137--146}, publisher = {IEEE Computer Society Press}, }

G. Castagna et G. Chen : Dependent types with subtyping and late-bound overloading. Information and Computation, vol. 168, n° 1, pag. 1-67, 2001.
[Abstract] We present a calculus with dependent types, subtyping and late-bound overloading. Besides its theoretical interest this work is motivated by several practical needs that range from the definition of logic encodings, to proof specialization and reuse, and to object-oriented extension of the SML module system. The theoretical study of this calculus is not straightforward. While confluence is relatively easy to prove, subject reduction is much harder. We were not able to add overloading to any existing system with dependent types and subtyping, and prove subject reduction. This is why we also define here as by-product a new subtyping system for dependent types that improves previous systems and enjoys several properties (notably the transitivity elimination property). The calculus with overloading is then obtained as a conservative extension of this new system. Another difficult point is strong normalization, which is a necessary condition to the decidability of subtyping and typing relations. The calculus with overloading is not strongly normalizing. However, we show that a reasonably useful fragment of the calculus enjoys this property, and that its strong normalization implies the decidability of its subtyping and typing relations. The article is divided into two parts: the first three sections provide a general overview of the systems and its motivations, and can be read separately; the remaining sections develop the formal study.[BibTeX] @article{CC99, author = {G. Castagna and G. Chen}, title = {Dependent types with subtyping and late-bound overloading}, journal = {Information and Computation}, year = {2001}, volume = {168}, number = {1}, pages = {1-67}, }

G. Castagna, G. Ghelli et F. Zappa Nardelli : Typing Mobility in the Seal Calculus. Dans CONCUR 2001, 12th. International Conference on Concurrency Theory, n° 2154, LNCS, pag. 82-101, Springer, 2001.
[Abstract] The issue of this work is how to type mobility, in the sense that we tackle the problem of typing not only mobile agents but also their movement. This yields higher-order types for agents. To that end we first provide a new definition of the Seal Calculus that gets rid of existing inessential features while preserving the distinctive characteristics of the Seal model. Then we discuss the use of interfaces to type agents and define the type system. The interpretation induced by this type system is that interfaces describe interaction effects rather than, as it is customary, provided services. We discuss at length the difference of the two interpretations and justify our choice of the former.[BibTeX] @inproceedings{CGZ01, author = {G. Castagna and G. Ghelli and F. {Zappa Nardelli}}, title = {Typing Mobility in the {S}eal {C}alculus}, booktitle = {{CONCUR} 2001, 12th.\ International Conference on Concurrency Theory}, year = {2001}, number = {2154}, series = {LNCS}, pages = {82-101}, address = {Aahrus, Danemark}, publisher = {Springer}, }

G. Castagna : Unifying overloading and λ-abstractions: λ^{}. Theoretical Computer Science, vol. 176, n° 1-2, pag. 337-345, avril, 1997.
[Abstract] In this short note we present a minimal system to deal with overloaded functions with late binding, in which λ-abstractions are seen as a special case of overloaded functions with just one code. We prove some relevant properties that this system enjoys, and show its connection with the λ&-calculus. We end by showing the practical interest of this system, in particular in modeling object-oriented languages.[BibTeX] @article{Cas96tcs, author = {G. Castagna}, title = {Unifying overloading and $\lambda$-abstractions: $\lambda^{\{\}}$}, journal = {Theoretical Computer Science}, year = {1997}, volume = {176}, number = {1-2}, pages = {337-345}, month = {apr}, }

G. Castagna et L. Liquori : A typed calculus of objects. Dans ASIAN '96, 1st Asian Computing Science Conference, n° 1179, LNCS, pag. 129-141, Springer, 1996.
[Abstract] In this paper, we present an explicitly typed version of the Lambda Calculus of Objects of Fisher, Honsell and Mitchell, which is a development of the object-calculi defined by Bruce and Longo. This calculus supports object extension in presence of object subsumption. Extension is the ability of modify the behavior of an object by adding new methods (and inheriting the existing ones). Object subsumption allows to use objects with a bigger interface in a context expecting another object with a smaller interface. This calculus has a sound and decidable type system, ``width'' subtyping, and it allows for first-class method bodies.[BibTeX] @inproceedings{LC96, author = {G. Castagna and L. Liquori}, title = {A typed calculus of objects}, booktitle = {ASIAN '96, 1st Asian Computing Science Conference}, year = {1996}, editor = {J.~Jaffar and R.~Yap}, number = {1179}, series = {LNCS}, pages = {129-141}, publisher = {Springer}, }

M.-V. Aponte et G. Castagna : Programmation modulaire avec surcharge et liaison tardive. Dans Journées Francophones des Langages Applicatifs, 1996.
[Abstract] One of the criticisms moved to the SML module system is that it does not allow code reusing and, more generally, and incremental style of programming. In this work we propose to extend this module system by adding overloading and late binding, and we show how by this extension it is possible to program modules in an incremental style, similar to the one of object-oriented languages.[BibTeX] @inproceedings{AC96, author = {M.-V. Aponte and G. Castagna}, title = {Programmation modulaire avec surcharge et liaison tardive}, booktitle = {Journ{é}es Francophones des Langages Applicatifs}, year = {1996}, address = {Val Morin, Qu{é}bec, Canada}, }

G. Castagna : Integration of parametric and ``ad hoc'' second order polymorphism in a calculus with subtyping. Formal Aspects of Computing, vol. 8, n° 3, pag. 247-293, 1996.
[Abstract] In this paper we define an extension of F_≤ to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit parametric polymorphism of F_≤ by an explicit ``ad hoc'' polymorphism (according the classification of Strachey). We prove that the calculus we obtain, called F^&_≤, enjoys the properties of Church-Rosser and Subject Reduction and that its proof system is coherent. We also define a significant subcalculus for which the subtyping is decidable. This extension has not only a logical interest but it is strongly motivated by the foundation of a broadly used programming style: object-oriented programming. The connections between F^&_≤ and object-oriented languages are widely stressed, and the modeling by F^&_≤ of some features of the object-oriented style is described, continuing the work on λ&.[BibTeX] @article{Cas93b, author = {G. Castagna}, title = {Integration of parametric and ``ad hoc'' second order polymorphism in a calculus with subtyping}, journal = {Formal Aspects of Computing}, year = {1996}, volume = {8}, number = {3}, pages = {247-293}, }

G. Castagna : Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, vol. 17, n° 3, pag. 431-447, 1995.
[Abstract] In type-theoretic research on object-oriented programming, the issue of ``covariance versus contravariance'' is a topic of continuing debate. In this short note we argue that covariance and contravariance appropriately characterize two distinct and independent mechanisms. The so-called contravariance rule correctly captures the subtyping relation (that relation which establishes which sets of functions can replace another given set in every context). A covariant relation, instead, characterizes the specialization of code (i.e., the definition of new code which replaces old definitions in some particular cases). Therefore, covariance and contravariance are not opposing views, but distinct concepts that each have their place in object-oriented systems. Both can (and should) be integrated in a type-safe manner in object-oriented languages. We also show that the independence of the two mechanisms is not characteristic of a particular model but is valid in general, since covariant specialization is present in record-based models, although it is hidden by a deficiency of all existing calculi that realize this model. As an aside, we show that the λ&-calculus can be taken as the basic calculus for both an overloading-based and a record-based model. Using this approach, one not only obtains a more uniform vision of object-oriented type theories, but in the case of the record-based approach, one also gains multiple dispatching, a feature that existing record-based models do not capture.[BibTeX] @article{Cas94, author = {G. Castagna}, title = {Covariance and contravariance: conflict without a cause}, journal = {ACM Transactions on Programming Languages and Systems}, year = {1995}, volume = {17}, number = {3}, pages = {431-447}, }

G. Castagna, G. Ghelli et G. Longo : A calculus for overloaded functions with subtyping. Information and Computation, vol. 117, n° 1, pag. 115-135, février, 1995.
[Abstract] We present a simple extension of typed λ-calculus where functions can be overloaded by putting different ``branches of code'' together. When the function is applied, the branch to execute is chosen according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that the branch selection depends on the ``run-time type'' of the argument, which may differ from its compile-time type, because of the existence of a subtyping relation among types. Hence overloading cannot be eliminated by a static analysis of code, but is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various λ-calculi where types do not play any role during computation. We prove Confluence and a generalized Subject-Reduction theorem for this calculus. We prove Strong Normalization for a ``stratified'' subcalculus. The definition of this calculus is guided by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensively stressed. We show that this calculus provides a foundation for typed object-oriented languages which solves some of the problems of the standard record-based approach.[BibTeX] @article{CGL94, author = {G. Castagna and G. Ghelli and G. Longo}, title = {A calculus for overloaded functions with subtyping}, journal = {Information and Computation}, year = {1995}, volume = {117}, number = {1}, pages = {115-135}, month = {feb}, }

G. Castagna et B.C. Pierce : Decidable Bounded Quantification. Dans POPL '94, 21st ACM Symposium on Principles of Programming Languages, pag. 151-162, ACM Press, janvier, 1994.
[Abstract] The standard formulation of bounded quantification, system F_≤, is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but those studied so far either exclude significant classes of useful programs or lack a compelling semantics. We propose here a simple variant of F_≤ that ameliorates these difficulties. It has a natural semantic interpretation, enjoys a number of important properties that fail in F_≤, and includes all of the programming examples for which F_≤ has been used in practice.[BibTeX] @inproceedings{CP93, author = {G. Castagna and B.C. Pierce}, title = {Decidable Bounded Quantification}, booktitle = {POPL '94, 21st ACM Symposium on Principles of Programming Languages}, year = {1994}, pages = {151-162}, address = {Portland, Oregon}, month = {jan}, publisher = {ACM Press}, }

G. Castagna : F_≤^& : integrating parametric and ``ad hoc'' second order polymorphism. Dans DBPL 4, 4th International Workshop on Database Programming Languages, Workshops in Computing, pag. 335-355, Springer, Sep, 1993. Contained in [Cas93b].
[Abstract] In the last years several object-oriented database systems have come to life. However among them there is a lack of statically strongly typed languages. This is a very important deficiency especially for languages, as the database programming languages, which are designed for complex applications of large size and that evolve in time. The absence of such a type discipline is justified by the complexity of the problem and of the structures it has to be applied to. Therefore we think that only a fundamental study, which were able to capture the essential features of the system, would lead to a typeful object-oriented programming. Thus we define an extension of F_≤ to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit parametric polymorphism of F_≤ by an explicit ``ad hoc'' polymorphism (according to the classification of [Str67]). We prove that the calculus we obtain, called F^&_≤, enjoys the properties of Church-Rosser and Subject Reduction. This extension constitutes our paradigmatic language for the foundation of object-oriented programming: the connections between F^&_≤ and object-oriented languages are widely stressed, and the modeling by F^&_≤ of some features of the object-oriented style is described.[BibTeX] @inproceedings{Cas93bea, author = {G. Castagna}, title = {${F}_{\leq}^{\&}$ : integrating parametric and ``ad hoc'' second order polymorphism}, booktitle = {DBPL 4, 4th International Workshop on Database Programming Languages}, year = {1993}, editor = {C. Beeri and A. Ohori and D. Shasha}, series = {Workshops in Computing}, pages = {335-355}, address = {New York City}, month = {Sep}, publisher = {Springer}, note = {Contained in~\cite{Cas93b}}, }

G. Castagna, G. Ghelli et G. Longo : A calculus for overloaded functions with subtyping. Dans ACM Conference on LISP and Functional Programming, pag. 182-192, ACM Press, juillet, 1992. Extended abstract of [CGL94].
[Abstract] We present a simple extension of typed λ-calculus where functions can be overloaded by adding different ``pieces of code''. In short, the code of an overloaded function is formed by several branches of code; the branch to execute is chosen, when the function is applied, according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that a subtyping relation is defined among types, such that the type of a term generally decreases during computation, and this fact induces a distinction between the ``compile-time'' type and the ``run-time'' type of a term. We study the case of overloaded functions where the branch selection depends on the run-time type of the argument, so that overloading cannot be eliminated by a static analysis of code, but is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various λ-calculi where types do not play, essentially, any rôle during computation. We prove Confluence and Strong Normalization for this calculus as well as a generalized Subject-Reduction theorem. The definition of this calculus is driven by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensively stressed. We show that this calculus provides a foundation for typed object-oriented languages which solves some of the problems of the standard record-based approach. It also provides a type-discipline for a relevant fragment of the ``core framework'' of CLOS.[BibTeX] @conference{CGL92, author = {G. Castagna and G. Ghelli and G. Longo}, title = {A calculus for overloaded functions with subtyping}, booktitle = {ACM Conference on LISP and Functional Programming}, year = {1992}, pages = {182-192}, address = {San Francisco}, month = {jul}, publisher = {ACM Press}, note = {Extended abstract of~\cite{CGL94}}, }

Théorie de la concurrence

G. Castagna, M. Dezani-Ciancaglini, E. Giachino et L. Padovani : 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] @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]

A. Phillips, L. Cardelli et G. Castagna : A Graphical Representation for Biological Processes in the Stochastic pi-calculus. Transactions on Computational Systems Biology, vol. 7, pag. 123-152, 2006.
[Abstract] This paper presents a graphical representation for the stochastic pi-calculus, which is formalised by defining a corresponding graphical calculus. The graphical calculus is shown to be reduction equivalent to stochastic pi, ensuring that the two calculi have the same expressive power. The graphical representation is used to model a couple of example biological systems, namely a bistable gene network and a mapk signalling cascade. One of the main benefits of the representation is its ability to highlight the existence of cycles, which are a key feature of many biological systems. Another benefit is its ability to animate interactions between system components, in order to visualise system dynamics. The graphical representation can also be used as a front end to a simulator for the stochastic pi-calculus, with a view to making modelling and simulation of biological systems more accessible to non computer scientists.[BibTeX] @article{PCC06, author = {A. Phillips and L. Cardelli and G. Castagna}, title = {A Graphical Representation for Biological Processes in the Stochastic pi-calculus}, journal = {Transactions on Computational Systems Biology}, year = {2006}, volume = {7}, pages = {123-152}, }

Langages de Programmation pour XML et Services Web

V. Benzaken, G. Castagna, D. Colazzo et C. Miachon : Pattern by Example: type-driven visual programming of XML queries. Dans PPDP '08: 10th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pag. 131―142, ACM, 2008.
[Abstract] We present Pattern-by-Example (PBE), a graphical language that allows users with little or no knowledge of pattern-matching and functional programming to define complex and optimized queries on XML documents. We demonstrate the key features of PBE by commenting an interactive session and then we present its semantics, by formally defining a translation from PBE graphical queries into CQL ones. The advantages of the approach are twofold. First, it generates queries that are provably correct with respect to types: the type of the result is displayed to the user and this constitutes a first and immediate visual check of the semantic correctness of the resulting query. The second advantage is that a semantics formally―thus, unambiguously―defined is an important advancement over some current approaches in which standard usage and learning methods are based on ``trial and error'' techniques[BibTeX] @inproceedings{BCM08, author = {V. Benzaken and G. Castagna and D. Colazzo and C. Miachon}, title = {{Pattern by Example}: type-driven visual programming of {XML} queries}, booktitle = {PPDP '08: 10th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming}, year = {2008}, pages = {131--142}, publisher = {ACM}, }

S. Carpineti, G. Castagna, C. Laneve et L. Padovani : A formal account of contracts for Web Services. Dans WS-FM, 3rd Int. Workshop on Web Services and Formal Methods, n° 4184, LNCS, pag. 148-162, Springer, 2006.
[Abstract] The Web Service Description Language (WSDL) and the Web Service Conversation Language (WSCL) provide standard technologies for describing the static and dynamic interfaces of Web services. In particular, they permit the specification of the valid sequences of messages―the contract―required to interact successfully with a Web service. However, neither of them provides a formal definition of contract. We define a formal contract language along with conformance and compliance relations so that clients conforming to a contract are able to complete interactions with services compliant with the same contract. Our contract language is suitable for publication in a WSDL interface or as a WSCL resource. We take CCS as the formal model which our investigation is based upon.[BibTeX] @inproceedings{CCLP06, author = {S. Carpineti and G. Castagna and C. Laneve and L. Padovani}, title = {A formal account of contracts for {Web} {S}ervices}, booktitle = {WS-FM, 3rd Int.\ Workshop on Web Services and Formal Methods}, year = {2006}, number = {4184}, series = {LNCS}, pages = {148-162}, publisher = {Springer}, }

G. Castagna, D. Colazzo et A. Frisch : Error Mining for Regular Expression Patterns. Dans ICTCS 2005, Italian Conference on Theoretical Computer Science, n° 3701, Lecture Notes in Computer Science, pag. 160-172, Springer, 2005.
[Abstract] In the design of type systems for XML programming languages based on regular expression types and patterns the focus has been over result analysis, with the main aim of statically checking that a transformation always yields data of an expected output type. While being crucial for correct program composition, result analysis is not sufficient to guarantee that patterns used in the transformation are correct. In this paper we motivate the need of static detection of incorrect patterns, and provide a formal characterization based on pattern matching operational semantics, together with locally exact type analysis techniques to statically detect them.[BibTeX] @inproceedings{CCF05, author = {G. Castagna and D. Colazzo and A. Frisch}, title = {Error Mining for Regular Expression Patterns}, booktitle = {ICTCS 2005, Italian Conference on Theoretical Computer Science}, year = {2005}, number = {3701}, series = {Lecture Notes in Computer Science}, pages = {160-172}, publisher = {Springer}, }

G. Castagna : Patterns and types for querying XML. Dans Proceedings of DBPL 2005, 10th International Symposium on Database Programming Languages Lecture Notes in Computer Science, n.3774, pages 1-26 Springer (full version) and XSym 2005, 3rd International XML Database Symposium Lecture Notes in Computer Science n.3671, pages 1-3, Springer (summary), 2005. Joint DBPL-XSym invited talk.
[Slides] [Abstract] Among various proposals for primitives for deconstructing XML data two approaches seem to clearly stem from practice: path expressions, widely adopted by the database community, and regular expression patterns, mainly developed and studied in the programming language community. We think that the two approaches are complementary and should be both integrated in languages for XML, and we see in that an opportunity of collaboration between the two communities. With this aim, we give a presentation of regular expression patterns and the type systems they are tightly coupled with. Although this article advocates a construction promoted by the programming language community, we will try to stress some characteristics that the database community, we hope, may find interesting.[BibTeX] @inproceedings{Cas05a, author = {G. Castagna}, title = {Patterns and types for querying {XML}}, booktitle = {\emph{Proceedings of} DBPL 2005, 10th International Symposium on Database Programming Languages \emph{Lecture Notes in Computer Science, n.3774, pages 1-26 Springer (full version)} and XSym 2005, 3rd International XML Database Symposium \emph {Lecture Notes in Computer Science n.3671, pages 1-3, Springer (summary)}}, year = {2005}, note = {Joint DBPL-XSym invited talk}, }

V. Benzaken, G. Castagna et C. Miachon : A Full Pattern-based Paradigm for XML Query Processing. Dans PADL 05, 7th International Symposium on Practical Aspects of Declarative Languages, n° 3350, LNCS, pag. 235―252, Springer, janvier, 2005.
[Abstract] In this article we investigate a novel execution paradigm―ML-like pattern-matching―for XML query processing. We show that such a paradigm is well adapted for a common and frequent set of queries and advocate that it constitutes a candidate for efficient execution of XML queries far better than the current XPath-based query mechanisms. We support our claim by comparing performances of XPath-based queries with pattern based ones, and by comparing the latter with the two efficiency-best XQuery processor we are aware of.[BibTeX] @inproceedings{BCM05, author = {V. Benzaken and G. Castagna and C. Miachon}, title = {A Full Pattern-based Paradigm for {XML} Query Processing}, booktitle = {PADL~05, 7th International Symposium on Practical Aspects of Declarative Languages}, year = {2005}, number = {3350}, series = {LNCS}, pages = {235--252}, month = {jan}, publisher = {Springer}, }

V. Benzaken, M. Burelle et G. Castagna : Information flow security for XML transformations. Dans ASIAN '03, 8th Asian Computing Science Conference, n° 2896, LNCS, pag. 33-53, Springer, décembre, 2003.
[Abstract] We provide a formal definition of information flows in XML transformations and, more generally, in the presence of type driven computations and describe a sound technique to detect transformations that may leak private or confidential information. We also outline a general framework to check middleware-located information flows.[BibTeX] @inproceedings{BBC03, author = {V. Benzaken and M. Burelle and G. Castagna}, title = {Information flow security for {XML} transformations}, booktitle = {ASIAN '03, 8th Asian Computing Science Conference}, year = {2003}, number = {2896}, series = {LNCS}, pages = {33-53}, month = {dec}, publisher = {Springer}, }

V. Benzaken, G. Castagna et A. Frisch : CDuce: an XML-Centric General-Purpose Language. Dans ICFP '03, 8th ACM International Conference on Functional Programming, pag. 51―63, ACM Press, 2003.
[Abstract] We present the functional language ℂDuce, discuss some design issues, and show its adequacy for working with XML documents. Distinctive features of ℂDuce are a powerful pattern matching, first class functions, overloaded functions, a very rich type system (arrows, sequences, pairs, records, intersections, unions, differences), precise type inference for patterns and error localization, and a natural interpretation of types as sets of values. We also outline some important implementation issues; in particular, a dispatch algorithm that demonstrates how static type information can be used to obtain very efficient compilation schemas.[BibTeX] @inproceedings{BCF03, author = {V. Benzaken and G. Castagna and A. Frisch}, title = {{CD}uce: an {XML}-Centric General-Purpose Language}, booktitle = {ICFP~'03, 8th ACM International Conference on Functional Programming}, year = {2003}, pages = {51--63}, address = {Uppsala, Sweden}, publisher = {ACM Press}, }

G. Castagna, J. Demouth, A. Frisch et S. Zacchiroli : ℂDuce User Manual, 2002-2015. Available on line at http://www.cduce.org/manual.html.
[BibTeX]@manual{cduceUM, author = {G. Castagna and J. Demouth and A. Frisch and S. Zacchiroli}, title = {\cduce{} User Manual}, year = {2002-2015}, note = {Available on line at \url{http://www.cduce.org/manual.html}}, }

V. Benzaken, G. Castagna et A. Frisch : ℂDuce Tutorial, 2002-2015. Available on line at http://www.cduce.org/tutorial.html.
[BibTeX]@manual{cduceTutorial, author = {V. Benzaken and G. Castagna and A. Frisch}, title = {\cduce{} Tutorial}, year = {2002-2015}, note = {Available on line at \url{http://www.cduce.org/tutorial.html}}, }

Mobilité et Distribution

G. Castagna, J. Vitek et F. Zappa Nardelli : The Seal Calculus. Information and Computation, vol. 201, n° 1, pag. 1―54, 2005.
[Abstract] The Seal Calculus is a process language for describing mobile computation. Threads and resources are tree structured; the nodes thereof correspond to agents, the units of mobility. The Calculus extends a π-calculus core with synchronous, objective mobility of agents over channels. This paper systematically compares all previous variants of Seal Calculus. We study their operational behaviour with labelled transition systems and bisimulations; by comparing the resulting algebraic theories we highlight the differences between these apparently similar approaches. This leads us to identify the dialect of Seal that is most amenable to operational reasoning and can form the basis of a distributed programming language. We propose type systems for characterising the communications in which an agent can engage. The type systems thus enforce a discipline of agent mobility, since the latter is coded in terms of higher-order communication.[BibTeX] @article{CVZ05, author = {G. Castagna and J. Vitek and F. Zappa~Nardelli}, title = {The {S}eal {C}alculus}, journal = {Information and Computation}, year = {2005}, volume = {201}, number = {1}, pages = {1--54}, }

M. Bugliesi, G. Castagna et S. Crafa : Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems, vol. 26, n° 1, pag. 57-124, 2004.
[Abstract] Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability, and introducing new primitives for ambient communication. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs in and out for mobility with finer-grained mechanisms for ambient interaction. We introduce the new calculus, study the impact of the new mechanisms for communication o typing and mobility, and show that they yield an effective framework for resource protection and access control in distributed systems.[BibTeX] @article{BCC04, author = {M. Bugliesi and G. Castagna and S. Crafa}, title = {Access Control for Mobile Agents: The {Calculus} of {Boxed} {Ambients}}, journal = {ACM Transactions on Programming Languages and Systems}, year = {2004}, volume = {26}, number = {1}, pages = {57-124}, }

G. Castagna et F. Zappa Nardelli : The Seal Calculus revisited: contextual equivalence and bisimilarity. Dans FST&TCS '02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science, n° 2556, LNCS, pag. 85―96, Springer, décembre, 2002.
[Abstract] We present a new version of the Seal Calculus, a calculus of mobile computation. We study observational congruence and bisimulation theory, and show how they are related.[BibTeX] @inproceedings{CZ02, author = {G. Castagna and F. {Zappa Nardelli}}, title = {The {Seal} {Calculus} revisited: contextual equivalence and bisimilarity}, booktitle = {{FST\&TCS} '02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science}, year = {2002}, number = {2556}, series = {LNCS}, pages = {85--96}, month = {dec}, publisher = {Springer}, }

Crafa, S., Bugliesi, M. et Castagna, G. : Information Flow Security for Boxed Ambients. Dans Foundations of Wide Area Network Computing (F-WAN), n° 66(3), Electronic Notes in Theoretical Computer Science, Elsevier Science B.V., 2002.
[Abstract] We study the problem of secure information flow for Boxed Ambients in terms of non-interference. The main contribution of this work is the study and the (type-based) control of new sources of information flow due to the interplay between communication and mobility, which is typical of network programming. We develop a sound type system that provides static guarantees of absence of unwanted flow of information for well typed processes. Non-interference is stated, and proved, in terms of a typed notion of contextual equivalence for Boxed Ambients akin to the corresponding equivalence defined for Mobile Ambients.[BibTeX] @inproceedings{CBC02, author = {Crafa, S. and Bugliesi, M. and Castagna, G.}, title = {Information Flow Security for {B}oxed {A}mbients}, booktitle = {Foundations of Wide Area Network Computing (F-WAN)}, year = {2002}, number = {66(3)}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science B.V.}, }

M. Bugliesi et G. Castagna : Behavioral Typing for Safe Ambients. Computer Languages, vol. 28, n° 1, pag. 61-99, novembre, 2002.
[Abstract] We introduce a typed variant of Safe Ambients, named Secure Safe Ambients (SSA), whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents. We study the type system of SSA, define algorithms for type checking and type reconstruction, define languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.[BibTeX] @article{BCcl, author = {M. Bugliesi and G. Castagna}, title = {Behavioral Typing for {S}afe {A}mbients}, journal = {Computer Languages}, year = {2002}, volume = {28}, number = {1}, pages = {61-99}, month = {nov}, }

G. Castagna : An overview of Boxed Ambients. Dans TOSCA '01, Theory of Concurrency, Higher Order, and Types Workshop, n° 62, Electronic Notes in Theoretical Computer Science, pag. 1-5, Elsevier Science B.V., 2001. Invited lecture based on joint work with M. Bugliesi and S. Crafa: [BCC01a,BCC01b].
[Abstract] In this lecture we present some work we did about mobility and hint at some new current lines of research on information flow and security. More precisely, we describe the calculus of Boxed Ambients a variant of Cardelli and Gordon's Mobile Ambients a calculus of mobile and dynamically reconfigurable agents. Boxed Ambients inherit from Mobile Ambients (part of) the mobility primitives but rely on a completely different model of communication. The new communication primitives fit nicely the design principles of Mobile Ambients, and complement the existing constructs for ambient mobility with finer-grained, and more effective, mechanisms for ambient interaction. As a result Boxed Ambients retain the expressive power and the computational flavor of Ambient Calculus, as well as the elegance of its formal presentation. In addition, they enhance the flexibility of typed communications over Mobile Ambients, and provide new insight into the relationship between synchronous and asynchronous input-output.[BibTeX] @inproceedings{Cas01, author = {G. Castagna}, title = {An overview of {B}oxed {A}mbients}, booktitle = {{TOSCA} '01, Theory of Concurrency, Higher Order, and Types Workshop}, year = {2001}, number = {62}, series = {Electronic Notes in Theoretical Computer Science}, pages = {1-5}, publisher = {Elsevier Science B.V.}, note = {Invited lecture based on joint work with M.~Bugliesi and S.~Crafa:~\cite{BCC01a,BCC01b}}, }

M. Bugliesi, G. Castagna et S. Crafa : Reasoning about security in Mobile Ambients. Dans CONCUR 2001, 12th. International Conference on Concurrency Theory, n° 2154, LNCS, pag. 102-120, Springer, 2001. Contained in [BCC04].
[Abstract] The paper gives an assessment of security for Mobile Ambients, with specific focus on mandatory access control (MAC) policies in multilevel security systems. The first part of the paper reports on different formalization attempts for MAC policies in the Ambient Calculus, and provides an in-depth analysis of the problems one encounters. As it turns out, MAC security does not appear to have fully convincing interpretations in the calculus. The second part proposes a solution to this impasse, based on a variant of Mobile Ambients. A type system for resource access control is defined, and the new calculus is discussed and illustrated with several examples of resource management policies.[BibTeX] @inproceedings{BCC01b, author = {M. Bugliesi and G. Castagna and S. Crafa}, title = {Reasoning about security in Mobile Ambients}, booktitle = {{CONCUR} 2001, 12th.\ International Conference on Concurrency Theory}, year = {2001}, number = {2154}, series = {LNCS}, pages = {102-120}, address = {Aahrus, Danemark}, publisher = {Springer}, note = {Contained in~\cite{BCC04}}, }

M. Bugliesi, G. Castagna et S. Crafa : Boxed Ambients. Dans TACS 2001, 4th. International Symposium on Theoretical Aspects of Computer Science, n° 2215, LNCS, pag. 38―63, Springer, 2001. Contained in [BCC04].
[Abstract] Boxed Ambients are a variant of Mobile Ambients, that result from (i) dropping the open capability and (ii) providing new primitives for ambient communication while retaining the constructs in and out for mobility. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs for Mobile Ambient mobility with finer-grained, and more effective, mechanisms for ambient interaction.[BibTeX] @inproceedings{BCC01a, author = {M. Bugliesi and G. Castagna and S. Crafa}, title = {Boxed Ambients}, booktitle = {{TACS} 2001, 4th.\ International Symposium on Theoretical Aspects of Computer Science}, year = {2001}, number = {2215}, series = {LNCS}, pages = {38--63}, address = {Sendai, Japan}, publisher = {Springer}, note = {Contained in~\cite{BCC04}}, }

M. Bugliesi, G. Castagna et S. Crafa : Subtyping and Matching for Mobile Objects. Dans ICTCS 2001, 7th. Italian Conference on Theoretical Computer Science, n° 2202, LNCS, pag. 235―255, Springer, 2001.
[Abstract] In a previous work we presented a general framework for extending calculi of mobile agents with object-oriented features, and we studied a typed instance of that model based on Cardelli and Gordon's Mobile Ambients. Here, we refine our earlier work and define a new calculus which is based on Remote Procedure Call as the underlying protocol for method invocation, and on a different typing technique for method bodies. The new type system is equipped with a subtyping and a matching relation: the combination of matching with subtyping provides new insight into the relationship between ambient opening in the new calculus and method overriding in object-oriented calculi.[BibTeX] @inproceedings{BCC01c, author = {M. Bugliesi and G. Castagna and S. Crafa}, title = {Subtyping and Matching for Mobile Objects}, booktitle = {{ICTCS} 2001, 7th.\ Italian Conference on Theoretical Computer Science}, year = {2001}, number = {2202}, series = {LNCS}, pages = {235--255}, address = {Torino, Italy}, publisher = {Springer}, }

M. Bugliesi et G. Castagna : Secure Safe Ambients. Dans POPL '01, 28th ACM Symposium on Principles of Programming Languages, pag. 222-235, ACM Press, 2001. Contained in [BCcl].
[Abstract] Secure Safe Ambients (SSA) are a typed variant of Safe Ambients, whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents. We study the type system of SSA, define algorithms for type checking and type reconstruction, define powerful languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.[BibTeX] @inproceedings{BC01, author = {M. Bugliesi and G. Castagna}, title = {Secure Safe Ambients}, booktitle = {POPL '01, 28th ACM Symposium on Principles of Programming Languages}, year = {2001}, pages = {222-235}, address = {London}, publisher = {ACM Press}, note = {Contained in~\cite{BCcl}}, }

M. Bugliesi, G. Castagna et S. Crafa : Typed Mobile Objects. Dans CONCUR 2000, 11th. International Conference on Concurrency Theory, n° 1877, LNCS, pag. 504-520, Springer, 2000.
[BibTeX]@inproceedings{BCC00, author = {M. Bugliesi and G. Castagna and S. Crafa}, title = {Typed Mobile Objects}, booktitle = {{CONCUR} 2000, 11th.\ International Conference on Concurrency Theory}, year = {2000}, number = {1877}, series = {LNCS}, pages = {504-520}, address = {Penn State University Parc}, publisher = {Springer}, }

G. Castagna et J. Vitek : Seal: A Framework for Secure Mobile Computations. Dans Internet Programming Languages, Springer, n° 1686, LNCS, pag. 47-77, 1999. Collected works.
[BibTeX]@incollection{CV99, author = {G. Castagna and J. Vitek}, title = {Seal: A Framework for Secure Mobile Computations}, booktitle = {Internet Programming Languages}, publisher = {Springer}, year = {1999}, editor = {H. Bal and B. Belkhouche and L. Cardelli}, number = {1686}, series = {LNCS}, pages = {47-77}, note = {Collected works\ifFRENCH\ [modalit{é}s de s{é}lection d'un num{é}ro sp{é}cial de revue. Assimilable {à} un article de revue internationale avec comit{é} de lecture]\else\fi}, }

G. Castagna : Types et Modèles : des langages objets séquentiels à la mobilité et à la sécurité, Université Paris 7, Habilitation à diriger des recherches, janvier, 2002.
[BibTeX]@phdthesis{Cas02hab, author = {G. Castagna}, title = {Types et {M}od{è}les : des langages objets s{é}quentiels {à} la mobilit{é} et {à} la s{é}curit{é}}, school = {Universit{é} Paris 7}, year = {2002}, type = {Habilitation {à} diriger des recherches}, month = {jan}, }

Bases de données

V. Benzaken, G. Castagna, L. Daynes, J. Lopez, K. Nguyễn et R. Vernoux : Language-integrated queries: a BOLDR approach. Dans Proceedings of the Web Conference (WWW2018), Web Programming track, avril, 2018.
[Abstract] We present BOLDR, a modular framework that enables the evaluation in, databases of queries containing application logic and, in particular,, user-defined functions. BOLDR also allows the nesting of queries for different, databases of possibly different data models. The framework detects the, boundaries of queries present in an application, translates them into an, intermediate representation together with the relevant language environment,, rewrites them in order to avoid query avalanches and to make the most out of, database optimizations, and converts the results back to the application. We, also present experiments showing that the techniques we implemented are, applicable to real-world database applications, both in terms of successfully, handling different sorts of language-integrated queries, and in terms of, better performance.[BibTeX] @inproceedings{boldr, author = {V. Benzaken and G. Castagna and L. Daynes and J. Lopez and K. Nguyễn and R. Vernoux}, title = {Language-integrated queries: a {BOLDR} approach}, booktitle = {Proceedings of the Web Conference ({WWW2018}), Web Programming track}, year = {2018}, month = {apr}, }

V. Benzaken, G. Castagna, D. Colazzo et K. Nguyễn : Type-Based XML Projection. Dans VLDB 2006, 32nd International Conference on Very Large Data Bases, pag. 271-282, 2006.
[Abstract] XML data projection (or pruning) is one of the main optimization techniques recently adopted in the context of main-memory XML query-engines. The underlying idea is quite simple: given a query Q over a document D, the subtrees of D not necessary to evaluate Q are pruned, thus obtaining a smaller document D'. Then Q is executed over D', hence avoiding to allocate and process nodes that will never be reached by navigational specifications in 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, which we devise in order to apply our solution. 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 DTDs, which include nearly all the queries used in the XMark and XPathMark benchmarks. These benchmarks are also used to test our implementation and show and gauge the practical benefits of our solution.[BibTeX] @inproceedings{BCCN06, author = {V. Benzaken and G. Castagna and D. Colazzo and K. Nguyễn}, title = {Type-Based {XML} Projection}, booktitle = {VLDB 2006, 32nd International Conference on Very Large Data Bases}, year = {2006}, pages = {271-282}, }

Bioinformatique

Securité

M. Bugliesi, G. Castagna, S. Crafa, R. Focardi et V. Sassone : Name-passing calculi and crypto-primitives: a survey. Dans Foundations of Security Analysis and Design, n° 2946, LNCS, pag. 91-138, Springer, 2004.
[BibTeX]@inproceedings{BCCFS04, author = {M. Bugliesi and G. Castagna and S. Crafa and R. Focardi and V. Sassone}, title = {Name-passing calculi and crypto-primitives: a survey}, booktitle = {Foundations of Security Analysis and Design}, year = {2004}, number = {2946}, series = {LNCS}, pages = {91-138}, publisher = {Springer}, }

J. Vitek et G. Castagna : Mobile Computations and Hostile Hosts. Dans Journées Francophones des Langages Applicatifs, pag. 113-132, Editions Hermès, 1999.
[Abstract] This paper scratches the surface of the problem of classifying the attacks that a mobile computation can be subjected to in an open network. The discussion is based on a simplified version of the Seal Calculus. We show how the impact of these attacks on the semantics of the calculus and on the notion of observational equivalence.[BibTeX] @inproceedings{VC99, author = {J.~Vitek and G. Castagna}, title = {Mobile Computations and Hostile Hosts}, booktitle = {Journ{é}es Francophones des Langages Applicatifs}, year = {1999}, pages = {113-132}, publisher = {Editions Herm{è}s}, }

Langages Orientés à Objets

J. Boyland et G. Castagna : Parasitic Methods: Implementation of Multi-Methods for Java. Dans OOPSLA '97, 12th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, vol. 32(10), pag. 66-76, 1997.
[Abstract] In an object-oriented programming language, method selection is (usually) done at run-time using the class of the receiver. Some object-oriented languages (such as CLOS) have multi-methods which comprise several methods selected on the basis of the run-time classes of all the parameters, not just the receiver. Multi-methods permit intuitive and type-safe definition of binary methods such as structural equality, set inclusion and matrix multiplication, just to name a few. Java as currently defined does not support multi-methods. This paper defines a simple extension to Java that enables the writing of ``encapsulated'' multi-methods through the use of parasitic methods, methods that ``attach'' themselves to other methods. Encapsulated multi-methods avoid some of the modularity problems that arise with fully general multi-methods. Furthermore, this extension yields for free both covariant and contravariant specialization of methods (besides Java's current invariant specialization). Programs using this extension can be translated automatically at the source level into programs that do not; they are modular, type-safe, and allow separate compilation.[BibTeX] @inproceedings{BC97, author = {J. Boyland and G. Castagna}, title = {Parasitic Methods: Implementation of Multi-Methods for {J}ava}, booktitle = {OOPSLA '97, 12th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications}, year = {1997}, volume = {32(10)}, pages = {66-76}, }

J. Boyland et G. Castagna : Type-safe compilation of covariant specialization: a practical case. Dans ECOOP '96, 10th European Conference on Object-Oriented Programming, n° 1098, LNCS, pag. 3-25, Springer, 1996.
[Abstract] Despite its lack of type safety, some typed object-oriented languages use covariant specialization for methods. In this work, we show how one may modify the semantics of languages that use covariant specialization in order to improve their type safety. We demonstrate our technique using O₂, a strongly and statically typed object-oriented database programming language which uses covariant specialization. We propose a modification to the O₂ compiler that adds code to correct previously ill-typed computations that arise from the use of covariant specialization. The modification we propose does not affect the semantics of those computations without type errors. Furthermore, the new semantics of the previously ill-typed computations is defined in a very ``natural'' way and ensures the type safety (w.r.t. covariance) of the program. Since the solution consists of a conservative backward-compatible modification of the compiler, it does not require, unlike other solutions, any modification of existing O₂ code. Our solution is based solely on a type-theoretic analysis and thus is general. Therefore, although this paper applies it to a particular programming language, the same ideas could easily be applied to other languages that use covariant specialization.[BibTeX] @inproceedings{Cas96, author = {J. Boyland and G. Castagna}, title = {Type-safe compilation of covariant specialization: a practical case}, booktitle = {ECOOP '96, 10th European Conference on Object-Oriented Programming}, year = {1996}, editor = {Pierre Cointe}, number = {1098}, series = {LNCS}, pages = {3-25}, publisher = {Springer}, }

K. Bruce, L. Cardelli, G. Castagna and The Hopkins Object Group, G. Leavens et B. Pierce : On Binary Methods. Theory and Practice of Object Systems, vol. 1, n° 3, pag. 221-242, 1996.
[Abstract] Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing binary methods, and collects and contrasts diverse views and solutions. It summarizes the current debate on the problem of binary methods for a wide audience.[BibTeX] @article{BruEtAl96, author = {K. Bruce and L. Cardelli and G. Castagna and The~Hopkins~Object~Group and G. Leavens and B. Pierce}, title = {On Binary Methods}, journal = {Theory and Practice of Object Systems}, year = {1996}, volume = {1}, number = {3}, pages = {221-242}, }

G. Castagna : A meta-language for typed object-oriented languages. Theoretical Computer Science, vol. 151, n° 2, pag. 297-352, novembre, 1995.
[Abstract] In [CGL94] we defined the λ&-calculus, a simple extension of the typed λ-calculus to model typed object-oriented languages. This paper is the continuation or, rather, the companion of  [CGL94] since it analyzes the practical counterpart of the theoretical issues introduced there. Indeed, to develop a formal study of type systems for object-oriented languages we define a meta-language based on λ& and we show, by a practical example, how it can be used it to prove properties of a language. To this purpose, we define a toy object-oriented language and its type-checking algorithm; then we translate this toy language into our meta-language. The translation gives the semantics of the toy language and a theorem on the translation of well-typed programs proves the correctness of the type-checker of the toy language. As an aside we also illustrate the expressivity of the λ&-based model by showing how to translate existing features like multiple inheritance and multiple dispatch, but also by integrating in the toy language new features directly suggested by the model, such as first-class messages, a generalization of the use of super and the use of explicit coercions. An important novelty with respect to previous systems is that we show how to model multiple dispatch also in the presence of a notion of receiver (i.e. of a privileged argument to which the message is passed), notion that is absent in languages like CLOS.[BibTeX] @article{Cas93, author = {G. Castagna}, title = {A meta-language for typed object-oriented languages}, journal = {Theoretical Computer Science}, year = {1995}, volume = {151}, number = {2}, pages = {297-352}, month = {nov}, }

G. Castagna : A meta-language for typed object-oriented languages. Dans FST&TCS '93, 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, n° 761, LNCS, pag. 52-71, Springer, décembre, 1993. Extended abstract of [Cas93].
[Abstract] In [CGL94] we defined the λ&-calculus, a simple extension of the typed λ-calculus to model typed object-oriented languages. To develop a formal study of type systems for object-oriented languages we define, in this paper, a meta-language based on λ& and we show by a practical example how to use it to prove properties of a language. To this purpose we define a toy object-oriented language and its type-checking algorithm; then we translate this toy language into our meta-language. The translation gives the semantics of the toy language and a theorem on the translation of well-typed programs proves the correction of the type-checker of the toy language. As an aside we also illustrate the expressivity of the λ&-based model by showing how to translate existing features like multiple inheritance and multiple dispatch, but also by integrating in the toy language new features directly suggested by the model, such as first-class messages, a generalization of the use of super and the use of explicit coercions.[BibTeX] @inproceedings{Cas93ea, author = {G. Castagna}, title = {A meta-language for typed object-oriented languages}, booktitle = {{FST\&TCS} '93, 13th Conference on the Foundations of Software Technology and Theoretical Computer Science}, year = {1993}, editor = {R.K. Shyamasundar}, number = {761}, series = {LNCS}, pages = {52-71}, address = {Bombay, India}, month = {dec}, publisher = {Springer}, note = {Extended abstract of~\cite{Cas93}}, }