Go up to Top
Go forward to References
Slides and Online Material
- The Programming Language
Core
(Slides)
A core imperative language, typing rules, induction and recursion, unicity of
typing, the typing rules define the language, the semantics of the core
language, soundness of the typing rules, operational properties of the
semantics, the design of a language core.
- The Abstraction Principle I
(Slides)
Expression abstractions, the semantics of abstractions, soundness of the
typing rules for abstractions, lazy evaluation and the copy rule, eager
evaluation, semantics of lazy and eager evaluation, other standard
abstractions, recursively defined abstractions.
- The Abstraction Principle II
(Slides)
Variable declarations, semantics of variables, type-structure abstractions,
semantics of type structures, declaration abstractions, the abstraction
principle is a record introduction principle,
- The Parameterization and Correspondence Principles
(Slides)
Expression parameters, semantics of parameter transmission, a copy rule for
lazily evaluated parameters, other varieties of parameters, type equivalence,
type-structure parameters, the correspondence principle, the semantics of
correspondence, parameter lists, the parameterization principle is a lambda
abstraction principle.
- The Qualification Principle
(Slides)
Command blocks, semantics of the command block, scope, semantics of dynamic
scoping, extent, declaration blocks, type-structure blocks, object-oriented
languages, semantics of dynamically scoped objects, subtyping,
the copy rule for blocks, the qualification principle is a record introduction
principle.
- Records and Lambda Abstractions
(Slides)
The desugared programming language, record introduction, lambda abstraction
introduction, higher-order programming languages, the semantics of records and
lambda abstractions, lazy evaluation semantics, eager evaluation semantics,
lazy and eager evaluation combined, lambda abstraction alone, orthogonality,
the model of the programming language, the logic of the programming language.
- On Understanding Types, Data Abstraction, and
Polymorphism
(Slides)
From untyped to typed universes, the typed lambda-calculus, universal
quantification and generic functions, existential quantification and
information hiding, bounded quantification and subtyping.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: types.tex,v 1.14 1996/06/13 14:10:50 schreine Exp schreine