A kernel language for modules and abstract data types

Rod Burstall and Butler Lampson


Citation: In Semantics of Data Types, Lecture Notes in Computer Science 173, Springer, 1984, pp 1-50. Also Digital SRC research report 1, September 1984.

A revised version appeared here.

Links: Abstract, Acrobat

Email: blampson@microsoft.com. This paper is at http://www.research.microsoft.com.



A small set of constructs can simulate a wide variety of apparently distinct features in modern programming languages. Using a kernel language called Pebble based on the typed lambda calculus with bindings, declarations, dependent types, and types as compile-time values, we show how to build modules, interfaces and implementations, abstract data types, generic types, recursive types, and unions. Pebble has a concise operational semantics given by inference rules.