On computing with types
Paul Tarau, David Haraburda · 2012
We express in terms of binary trees seen as Gödel System T types (with the empty type as the only primitive type) arithmetic computations within time and space bounds comparable to binary arithmetic and derive an efficiently testable total ordering on types, isomorphic to the ordering of natural numbers.