Podcasts Technology Iowa Type Theory Commute Explaining my encoding of a HOAS datatype, part 1

Explaining my encoding of a HOAS datatype, part 1

Published: Oct. 19, 2020, 10 p.m.

b'

I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.\\xa0 The goal is to encode a datatype (including its constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submit is the simplest higher-order datatype possible.\\xa0 I just explain some of the setup, and will attempt wading through the details next time.

'