Iowa Type Theory Commute
Explaining my encoding of a HOAS datatype, part 2
Nov 09, 2020
Season 2
Episode 8
Aaron Stump
I continue discussing the approach to HOAS from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.