> There is also PHOAS, which is a bit more lightweight. (Adam Chlipala,
> Parameterized Higher Order Abstract Syntax for Mechanized Semantics).
> I have started a translation of the paper in Agda:
Of course type-in-type results in an unsound logic, tho :-(
Stefan