Flemming Nielson6 and Hanne Riis Nielson6
| (6) |
Department of Computer Science, Aarhus University, Denmark |
Abstract
The design and implementation of a correct system can benefit from employing static techniques for ensuring that the dynamic
behaviour satisfies the specification. Many programming languages incorporate types for ensuring that certain operations are
only applied to data of the appropriate form. A natural extension of type checking techniques is to enrich the types with
annotations and effects that further describe intensional aspects of the dynamic behaviour.
Keywords Polymorphic type systems - effect annotations - subeffecting and subtyping - semantic correctness - type inference algorithms - syntactic soundness and completeness - Analyses for control flow - binding times - side effects - region structure - communication structure
Acknowledgements We wish to thank Torben Amtoft for working with us for many years on type and effect systems; we would also like to thank
the referees for their careful reading and helpful comments.
References secured to subscribers.