Daniel O. Martínez-Rivillas

A Theory of a Two-Dimensional Typed Lambda Calculus

We present a typed two-dimensional $\lambda$-calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (the $\beta$- and $\eta$-contractions, the congruences, and the structural rules), and every property of paths is proved \emph{by recursi...