Elegant elaboration with function invocation

Abstract

We present an elegant design of the core language in a dependently-typed lambda calculus with $\delta$-reduction and an elaboration algorithm.

6 pages, 3 figures