Alexei Pavlovich Kopylov
Type Theoretical Foundations for Data Structures, Classes, and Objects.
PhD Thesis, Cornell University, 2004.
(Also available as Technical
Report TR 2004-1923, Cornell University)
In this thesis we explore the question of how to represent
programming data structures in a constructive type theory. The basic
data structures in programing languages are records and objects. Most
known papers treat such data structure as primitive. That is, they add
new primitive type constructors and supporting axioms for records and
objects. This approach is not satisfactory. First of all it complicates
a type theory a lot. Second, the validity of the new axioms is not
easily established. As we will see the naive choice of axioms can lead
to contradiction even in the simplest cases.
We will show that records and objects can be defined in a powerful enough type theory. We will also show how to use these type constructors to define abstract data structure.