Generating Bijections between HOAS and the Natural Numbers

Details Generating Bijections between HOAS and the Natural Numbers Generating Bijections between HOAS and the Natural Numbers

2010-09-14

arxiv.org/abs/1009.2790v1

EPTCS 34, 2010, pp. 21-35

Computer Science

Logic in Computer Science

In Proceedings LFMTP 2010, arXiv:1009.2189

Scientific paper

10.4204/EPTCS.34.4

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 many situations and are preferably provided in a library of some sort. I have released a map and set library for use with Twelf which can be used with any type for which a bijection to the natural numbers exists. Since creating such bijections is tedious and error-prone, I have created a "bijection generator" that generates such bijections automatically together with proofs of correctness, all in the context of Twelf.

Affiliated with

Also associated with

No associations

Rating

Generating Bijections between HOAS and the Natural Numbers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Generating Bijections between HOAS and the Natural Numbers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Generating Bijections between HOAS and the Natural Numbers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-76503