Giuseppe CastagnaSenior Research Scientist
CNRS
Université Paris Cité
IRIF
Tel : +33 1 5727 9340
Fax: +33 1 5727 9297
beppe
irif.fr
Giuseppe Castagna's Home Page
Current Interests
Programming languages, models of computation, language level security, mobility, type theory, object-oriented programming, process algebras, languages for XML, web-services.
Honors and awards
- Member peer elected at the Academia Europæa, section B2: INFORMATICS.
- CACM Research Highlights nomination by ACM SIGPLAN for the article “Set-Theoretic Foundation of Parametric Polymorphism and Subtyping" presented at the ICFP '11, the 16th ACM-SIGPLAN International Conference on Functional Programming, 2011.
- Most Influential Paper 10-Year Award (2019) for the article “Foundation of Session Types" presented at the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2009.
Publications
- Publications by type: non exhaustive list containing at least the main references
- Publications by topic: the same publications ordered by their topic
- Latest papers: a selection of most recent and possibly unpublished work
- Selected papers: some papers I am proud of.
Recent Professional Service
- IRIF
: Research Institute on the Foundations of Computer Science (Director) - Section 6 du Comité National de la Recherche Scientifique (CoNRS ): member [2012-2016]
- ANVUR : Italian National Agency
for the Evaluation of Universities and Research Institutes. GEV01 member [2011-2013]
- PACMPL Proceedings of the ACM on Programming Languages, Editorial Board member
- POPL (Steering Committee Chair [2017-2018], Member [2015-2019])
- ESOP (Steering Commitee Chair [2013-2017] )
- ECOOP (Steering Committee member)
- ETAPS (Steering Committee member [2007-2017])
- POPL 2017 (General Chair )
- ECOOP 2013 (Program Committee Chair )
- ESOP 2009 (Program Committee Chair )
Some Links
- WGT 2020 : First ACM SIGPLAN Workshop on Gradual Typing , co-hosted with POPL 2020.
- A course on Four kinds of polymorphism: parametric, subtyping, ad-hoc, and gradual typing. SIGPL Summer School 2019 . Have a look at my slides.
- The ℂDuce project: a language for type-safe and fast query and transformation of XML documents
- Typex Typeful and certified XML (ANR Project)
- BETTY Behavioural Types for Reliable Large-Scale Software Systems (ICT COST Action)
- Codex Efficiency, Dynamicity and Composition for XML: Models, Algorithms and Systems (ANR Project)
- ITRS 2012 (Invited speaker)
- FMOODS & FORTE 2011 (Invited speaker)(paper) (slides)
- SBLP 2007 (Invited speaker) (slides)
- ICALP /PPDP 2005 (Joint keynote speaker) (paper) (slides)
- DBPL /XSYM 2005 (Joint Invited speaker) (paper) (slides)
- ICTCS 2005 (Invited speaker) (paper)
Latest Papers (February 2023)
: Programming with union, intersection, and negation types, December, 2022. Unpublished manuscript (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] Click for bibtex entry@unpublished{Cas22, author = {Giuseppe Castagna}, title = {Programming with union, intersection, and negation types}, note = {Unpublished manuscript (\href{https://arxiv.org/abs/2111.03354}{arXiv:2111.03354})}, month = {dec}, year = {2022}, }
[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] Click for bibtex entry@unpublished{Cas22, author = {Giuseppe Castagna}, title = {Programming with union, intersection, and negation types}, note = {Unpublished manuscript (\href{https://arxiv.org/abs/2111.03354}{arXiv:2111.03354})}, month = {dec}, year = {2022}, }
: On Type-Cases, Union Elimination, and Occurrence Typing. Proc. ACM Program. Lang., vol. 6, n. POPL, January, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
: 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]Click for bibtex entry@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}}, }
[BibTeX]Click for bibtex entry@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}}, }
: Revisiting Occurrence Typing. Science of Computer Programming, vol. 217, pag. 102781, March, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
: 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
: Foundations of Session Types: 10 Years Later. In 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]Click for bibtex entry@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}}, }
[BibTeX]Click for bibtex entry@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}}, }
: A space-efficient call-by-value virtual machine for gradual set-theoretic types. In IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages, September, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
: Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, Article 16, n. POPL '19: 46th ACM Symposium on Principles of Programming Languages, January, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
: Semantic subtyping for non-strict languages. In 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
|
|
