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