Alan Mycroft
Computer Laboratory
University of Cambridge
United Kingdom
Type-Like Frameworks for Controlling State and Aliasing
Abstract
Dijkstra's famous maxim "go to statement considered harmful" noted that spaghetti-like code was hard to reason about. However, in the presence of side effects and (especially) concurrency, spaghetti-like data is far harder to understand - not only in terms of the full behaviour of a program but also in terms of lesser properties such as performance prediction on multicore architectures. We present various compile-time techniques for controlling stateful operations and investigate some of their connections. These techniques include sub-structural type systems, effect systems, typestate, session types, contracts, linear and quasi-linear types, monads, separation logic and ownership types.
Course materials in EWSCS'10 handouts
- A. Mycroft. Types for state and aliasing: a 4-lecture introduction. Slides, 2010. [pdf]
- R. J. Ennals, R. W. Sharp, A. Mycroft. Linear types for packet processing. In D. A. Schmidt, ed., Proc. of ESOP 2004, v. 2986 of Lect. Notes in Comput. Sci., pp. 204-218. Springer, 2004. [doi link]
- D. G. Clarke, J. M. Potter, J. Noble. Ownership types for flexible alias protection. In Proc. of OOPSLA '98, pp. 48-64. ACM Press, 1998. [doi link]
- S. Srinivasan, A. Mycroft. Kilim: isolation-typed actors for Java. In J. Vitek, ed., Proc. of ECOOP 2008, v. 5142 of Lect. Notes in Comput. Sci., pp. 104-128. Springer, 2008. [doi link]
More course materials
- J. Aldrich, J. Sunshine, D. Saini, Z. Sparks. Typestate-oriented programming. In Companion to OOPSLA '09, pp. 1015-1022. ACM Press, 2009. [doi link]
- J. M. Lucassen, D. K. Gifford. Polymorphic effect systems. In Proc. of POPL '88, pp. 47-57. ACM Press, 1998. [doi link]
- N. Kobayashi. Quasi-linear types. In Proc. of POPL '99, pp. 29-42. ACM Press, 1999. [doi link]
- J. C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proc. of LICS '02, pp. 55-74. IEEE CS Press, 2002. [doi link]
- P. Wadler. Linear types can change the world! In M. Broy, C. Jones, eds., Programming Concepts and Methods, pp. 561-581. North-Holland, 1990.
- P. Wadler. The essence of functional programming. In Proc. of POPL '92, pp. 1-14. ACM Press, 1992. [doi link]
Last changed
March 7, 2010 22:27 EET
by
local organizers, ewscs10(at)cs.ioc.ee
EWSCS'10 page:
http://cs.ioc.ee/ewscs/2010/