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
- Erlang 2023 , invited talk: A type system for Elixir. The slides of the talk and the paper the talk is based on.
- 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 (September 2023)
: Polymorphic Type Inference for Dynamic Languages, July, 2023. Unpublished manuscript.
[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] Click for bibtex entry@unpublished{CLN23, author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn}, title = {Polymorphic Type Inference for Dynamic Languages}, note = {Unpublished manuscript}, month = {jul}, year = {2023}, }
[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] Click for bibtex entry@unpublished{CLN23, author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn}, title = {Polymorphic Type Inference for Dynamic Languages}, note = {Unpublished manuscript}, month = {jul}, year = {2023}, }
: Programming with union, intersection, and negation types. In The French School of Programming, Springer, August, 2023. 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] Click for bibtex entry@incollection{Cas22, author = {Giuseppe Castagna}, title = {Programming with union, intersection, and negation types}, booktitle = {The French School of Programming}, publisher = {Springer}, year = {2023}, editor = {Bertrand Meyer}, month = {aug}, note = {ISBN 978-3-031-34517-3. Preprint at \href{https://arxiv.org/abs/2111.03354}{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@incollection{Cas22, author = {Giuseppe Castagna}, title = {Programming with union, intersection, and negation types}, booktitle = {The French School of Programming}, publisher = {Springer}, year = {2023}, editor = {Bertrand Meyer}, month = {aug}, note = {ISBN 978-3-031-34517-3. Preprint at \href{https://arxiv.org/abs/2111.03354}{arXiv:2111.03354}}, }
: The Design Principles of the Elixir Type System. The Art, Science, and Engineering of Programming, vol. 8, n. 2, 2024. To appear. Preprint in ArXiv: arXiv:2306.06391. Presentation given 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] Click for bibtex entry@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 = {To appear. Preprint in ArXiv: \href{https://arxiv.org/abs/2306.06391}{arXiv:2306.06391}. Presentation given at ElixirConf EU 2023: \url{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] Click for bibtex entry@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 = {To appear. Preprint in ArXiv: \href{https://arxiv.org/abs/2306.06391}{arXiv:2306.06391}. Presentation given at ElixirConf EU 2023: \url{https://www.youtube.com/watch?v=gJJH7a2J9O8}}, }
: Typing Records, Maps, and Structs. Proc. ACM Program. Lang., vol. 7, n. ICFP, September, 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] Click for bibtex entry@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}}, }
[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] Click for bibtex entry@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}}, }
: 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}, }
|
|
