A Theory Supporting Higher Order Abstract Syntax

by Brown, Wednesday, August 19, 2020, 09:59 (473 days ago)

In early August I published a new theory into the chain. I call the theory HOAS (for Higher Order Abstract Syntax) and it has infrastructure to define syntactic things like programming languages and more "semantic" things like their operational semantics. As a small example I embedded untyped lambda calculus into the theory, defined beta equivalence and conjectured and then proved the existence of a fixed point operator.

I wrote a description as a technical report available here:

http://grid01.ciirc.cvut.cz/~chad/hoas/pfghoas.pdf

I may update it if given feedback.

A colleague and I last week defined a version of the Dedukti framework language and its typechecking relation within the HOAS theory. We might write more about this soon, but it will depend on the tech report above.

I also have some other ideas for what to use the theory for and will make posts for the ideas that seem to be potentially fruitful.