Dear Type Theorists and Practioners,
I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.)
Thank you in advance,
Andrei Popescu