zbMATH — the first resource for mathematics

Types as theories. (English) Zbl 0792.68100
Topology and category theory in computer science, Proc. Conf., Oxford/UK 1989, 357-390 (1991).
Summary: [For the entire collection see Zbl 0725.00017.]
There are many notions of type in computing. The most classical notion is ‘types as sets’, which has been extended to cover many features of modern programming languages. The article shows that such features are handled perhaps even more naturally by an extension of the ‘types as algebras’ notion to a ‘types as theories’ notion. This notion naturally supports object-oriented concepts, including inheritance and local state, as well as generic modules and dependent types. Moreover, it explains why polymorphic operations are natural transformations and provides a systematic foundation for a powerful form of programming in the large. This chapter also suggests a new semantics for dependent types based on strict fibrations.

68Q65 Abstract data types; algebraic specification
68Q55 Semantics in the theory of computing
PDF BibTeX Cite