Combining programming with theorem proving
Chiyan Chen, Hongwei Xi · 2005
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