Polymorphic Subtyping for Side Effects
DOI:
https://doi.org/10.7146/dpb.v26i529.7058Resumé
The integration of polymorphism (in the style of the ML let-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. This paper presents a type system for (a core subset of) Concurrent~ML that extends the ML type system in a conservative way and that employs all these features; and in addition causality information has been incorporated into the effects (which may therefore be termed "behaviours").
The semantic soundness of the system is established via a subject reduction result. An inference algorithm is presented; it is proved sound and (in a certain sense) also complete. A prototype system based on this algorithm has been implemented and can be experienced on the WWW; thanks to a special post-processing phase it produces quite readable and informative output.
Downloads
Publiceret
Citation/Eksport
Nummer
Sektion
Licens
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.