Combining programming with theorem proving

Abstract

1. Introduction The notion of type equality plays a pivotal r^ole in type systemdesign. However, the importance of this role is often less evident in commonly studied type systems. For instance, in the simplytyped