Giuseppe Castagna Senior Research Scientist CNRS Université Paris Cité IRIF Tel : +33 1 5727 9340
Fax: +33 1 5727 9297 beppeirif.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.
Giuseppe Castagna: 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},
}
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze: 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},
}
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and 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]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}},
}
G. Castagna, M. Laurent, V. Lanvin, and K. Nguyễn: 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},
}
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] 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},
}
Giuseppe Castagna, Mariangola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani: 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}},
}
G. Castagna, G. Duboc, V. Lanvin, and J. G. Siek: 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},
}
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and 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, 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},
}
Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca: 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},
}