Object-Oriented Programming in Dependent Type Theory
Anton Setzer · Intellect Books · 2005
Abstract: We introduce basic concepts from object-oriented programming into dependent type theory based on the idea of modelling objects as interactive programs. We consider methods, interfaces, and the interaction between a fixed number of objects, including self-referential method calls. We introduce a monad like syntax for developing objects in dependent type theory. 1.1