Selected publications
[ Page automatically generated on Friday, 12 July 2024 from the following file(s): /home/beppe/BIBLIO/castagna-unp.bib /home/beppe/BIBLIO/castagna.bib ]
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}, }
[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, 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}, }
[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}, }
G. Castagna, K. Nguyễn, Z. Xu, and P. Abate: Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. In POPL '15, 42nd ACM Symposium on Principles of Programming Languages, pag. 289―302, January, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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, and L. Padovani: Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In POPL '14, 41st ACM Symposium on Principles of Programming Languages, pag. 5―17, January, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
G. Castagna and Z. Xu: Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, September, 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] Click for bibtex entry@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]
[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] Click for bibtex entry@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]
A. Frisch, G. Castagna, and 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] Click for bibtex entry@article{FCB08, author = {A. Frisch and G. Castagna and V. Benzaken}, title = {Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types}, journal = {Journal of the ACM}, year = {2008}, volume = {55}, number = {4}, pages = {1--64}, }
[Slides] [Abstract] Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean connectives, functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm.[BibTeX] Click for bibtex entry@article{FCB08, author = {A. Frisch and G. Castagna and V. Benzaken}, title = {Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types}, journal = {Journal of the ACM}, year = {2008}, volume = {55}, number = {4}, pages = {1--64}, }
G. Castagna, R. De Nicola, and 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] Click for bibtex entry@article{CDV08, author = {G. Castagna and R. {De Nicola} and D. Varacca}, title = {Semantic subtyping for the $\pi$-calculus}, journal = {Theoretical Computer Science}, year = {2008}, volume = {398}, number = {1-3}, pages = {217-242}, note = {Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca}, }
[Abstract] Subtyping relations for the π-calculus are usually defined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping relation. The type system we consider includes read-only and write-only channel types, as well as boolean combinations of types. A set-theoretic interpretation of types is provided, in which boolean combinations of types are interpreted as the corresponding set-theoretic operations. Subtyping is defined as inclusion of the interpretations. We prove the decidability of the subtyping relation and sketch the subtyping algorithm. In order to fully exploit the type system, we define a variant of the π-calculus where communication is subjected to pattern matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@article{CDV08, author = {G. Castagna and R. {De Nicola} and D. Varacca}, title = {Semantic subtyping for the $\pi$-calculus}, journal = {Theoretical Computer Science}, year = {2008}, volume = {398}, number = {1-3}, pages = {217-242}, note = {Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca}, }
G. Castagna: Semantic subtyping: challenges, perspectives, and open problems. In 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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 and A. Frisch: A gentle introduction to semantic subtyping. In 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), July, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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, J. Vitek, and 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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, and 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
V. Benzaken, G. Castagna, and A. Frisch: CDuce: an XML-Centric General-Purpose Language. In 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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 and 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
K. Bruce, L. Cardelli, G. Castagna and
The Hopkins Object Group, G. Leavens, and 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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: 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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, and G. Longo: A calculus for overloaded functions with subtyping. Information and Computation, vol. 117, n. 1, pag. 115-135, February, 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] Click for bibtex entry@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}, }
[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] Click for bibtex entry@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}, }
|
|
