In this paper, a notation influenced by de Bruijn's syntax of the ?-calculus is used to describe canonical forms of terms and an equivalence relation which divides terms into classes according to their reductional behaviour. We show that this notation helps describe canonical forms more elegantly than the classical notation and we establish the desirable properties of our reduction modulo equivalence classes rather than single terms. Finally, we extend the cube consisting of eight type systems with class reduction and show that this extension satisfies all the desirable properties of type systems.
|Title of host publication||Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming|
|Number of pages||12|
|Publication status||Published - 2001|
|Event||Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) - Florence, Italy|
Duration: 5 Sep 2001 → 7 Sep 2001
|Conference||Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)|
|Period||5/09/01 → 7/09/01|