Interactive Programs in Dependent Type Theory

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.

• Type: Conference
• Year: 2000
• Where: CSL
• Authors: Peter Hancock, Anton Setzer
• Keywords: Automated Reasoning, CSL 2000, Dependent Type Theory, Object-oriented Programming, Self-referential Method Calls