## Generating Bijections Between HOAS and the Natural Numbers

by John Boyland.

### Abstract

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. Since creating such bijections is tedious and error-prone, we have
created a ``bijection generator'' that generates such bijections
automatically together with proofs of correctness, all in the context
of Twelf.

### BibTeX Style Reference

@inproceedings(boyland:10map-natural,
author = {John Boyland}
title = {Generating Bijections between HOAS and the Natural Numbers},
booktitle = {LFMTP: Logical Frameworks and Meta-languages: Theory and Practice},
month = jul,
year = 2010)

### How to Get a Copy

The proceedings version of the paper
is in available in PDF.

### The Software

The software is available.

Last Modified: January 3, 2011

Generating Bijections Between HOAS and the Natural Numbers /
boyland@cs.uwm.edu