De Bruijn's syntax and reductional equivalence of λ-terms

Fairouz Kamareddine, Roel Bloo, Rob Nederpelt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages16-27
Number of pages12
Publication statusPublished - 2001
EventProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) - Florence, Italy
Duration: 5 Sep 20017 Sep 2001

Conference

ConferenceProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)
CountryItaly
CityFlorence
Period5/09/017/09/01

Fingerprint Dive into the research topics of 'De Bruijn's syntax and reductional equivalence of λ-terms'. Together they form a unique fingerprint.

  • Cite this

    Kamareddine, F., Bloo, R., & Nederpelt, R. (2001). De Bruijn's syntax and reductional equivalence of λ-terms. In Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (pp. 16-27)