Generating Bijections between HOAS and the Natural Numbers

A provably correct bijection between higher-order abstract syntax (HOAS) and the natural numbers enables one to define a ``not equals'' relationship between terms and also to have an adequate encoding of sets of terms, and maps from one term family to another. Sets and maps are useful in m...

Full description

Bibliographic Details
Main Author: John Tang Boyland
Format: Article
Language:English
Published: Open Publishing Association 2010-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1009.2790v1