In my view lambda calculus is a perfect match for AIT since the language is both so simple and so expressive. This should be readily apparent from the concise self-interpreter. The versions of AIT that you've seen based on TMs probably didn't have any explicit constants because determining them would be much too cumbersome. Chaitin was the first to prove theorems in AIT with actual programs and he resorted to LISP. I'm positioning lambda calculus as an even better choice.