Syntactic soundness proof of a type-and-capability system with hidden state

Abstract : This paper presents a formal definition and machine-checked soundness proof for a very expressive type-and-capability system, that is, a low-level type system that keeps precise track of ownership and side effects. The programming language has first-class functions and references. The type system's features include: universal, existential, and recursive types; subtyping; a distinction between affine and unrestricted data; support for strong updates; support for naming values and heap fragments, via singleton and group regions; a distinction between ordinary values (which exist at runtime) and capabilities (which don't); support for dynamic re-organizations of the ownership hierarchy, by dis-assembling and re-assembling capabilities; support for temporarily or permanently hiding a capability, via frame and anti-frame rules. One contribution of the paper is the definition of the type-and-capability system itself. We present the system as modularly as possible. In particular, at the core of the system, the treatment of affinity, in the style of dual intuitionistic linear logic, is formulated in terms of an arbitrary monotonic separation algebra, a novel axiomatization of resources, ownership, and the manner in which they evolve with time. Only the peripheral layers of the system are aware that we are dealing with a specific monotonic separation algebra, whose resources are references and regions. This semi-abstract organization should facilitate further extensions of the system with new forms of resources. The other main contribution is a machine-checked proof of type soundness. The proof is carried out in Wright and Felleisen's syntactic style. This offers evidence that this relatively simple-minded proof technique can scale up to systems of this complexity, and constitutes a viable alternative to more sophisticated semantic proof techniques. We do not claim that the syntactic technique is superior: we simply illustrate how it is used and highlight its strengths and shortcomings.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2013, 23 (1), pp.38-144. <10.1017/S0956796812000366>
Liste complète des métadonnées

https://hal.inria.fr/hal-00877589
Contributeur : François Pottier <>
Soumis le : lundi 28 octobre 2013 - 21:36:01
Dernière modification le : lundi 5 octobre 2015 - 16:58:26
Document(s) archivé(s) le : mercredi 29 janvier 2014 - 04:50:25

Fichier

fpottier-ssphs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

François Pottier. Syntactic soundness proof of a type-and-capability system with hidden state. Journal of Functional Programming, Cambridge University Press (CUP), 2013, 23 (1), pp.38-144. <10.1017/S0956796812000366>. <hal-00877589>

Partager

Métriques

Consultations de
la notice

229

Téléchargements du document

113