Computational foundations of basic recursive function theoryUsing reflection to explain and enhance type theory
