<p>The formal system λδ is a typed λ-calculus that
pursues the unification of terms, types, environments and contexts
<p>The formal system λδ is a typed λ-calculus that
pursues the unification of terms, types, environments and contexts