Types and programming languages /
A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective -- -has important applicat...
| Основен автор: | Pierce, Benjamin C. |
|---|---|
| Формат: | Книга |
| Език: | English |
| Публикувано: |
Cambridge, Mass. :
MIT Press,
2002.
|
| Предмети: | |
| Онлайн достъп: |
ebrary |
Съдържание:
- 1.
- Introduction
- 2.
- Mathematical preliminaries
- [pt]. 1.
- Untyped systems
- 3.
- Untyped arithmetic expressions
- 4.
- An ML implementation of arithmetic expressions
- 5.
- The untyped Lambda-calculus
- 6.
- Nameless representation of terms
- 7.
- An ML implementation of the Lambda-calculus
- [pt]. 2.
- Simple types
- 8.
- Typed arithmetic expressions
- 9.
- Simply typed Lambda-calculus
- 10.
- An ML implementation of simple types
- 11.
- Simple extensions
- 12.
- Normalization
- 13.
- References
- 14.
- Exceptions
- [pt]. 3.
- Subtyping
- 15.
- Subtyping
- 16.
- Metatheory of subtyping
- 17.
- An ML implementation of subtyping
- 18.
- Case study : imperative objects
- 19.
- Case study : featherweight Java
- [pt]. 4.
- Recursive types
- 20.
- Recursive types
- 21.
- Metatheory of recursive types
- [pt.]. 5.
- Polymorphism
- 22.
- Type reconstruction
- 23.
- Universal types
- 24.
- Existential types
- 25.
- An ML implementation of system F
- 26.
- Bounded quantification
- 27.
- Case study : imperative objects, redux
- 28.
- Metatheory of bounded quantification
- [pt]. 6.
- Higher-order systems
- 29.
- Type operators and kinding
- 30.
- Higher-order polymorphism
- 31.
- Higher-order subtyping.