Absolute explicit unification

Abstract

This paper presents a system for explicit substitutions in Pure Type Systems (PTS). The system allows to solve type checking, type inhabitation, higher-order unification, and type inference for PTS using purely first-order machinery. A novel feature of our system is that it combines substitutions and variable declarations. This allows as a side-effect to type check let-bindings. Our treatment of meta-variables is also explicit, such that instantiations of meta-variables is internalized in the calculus. This produces a confluent λ-calculus with distinguished holes and explicit substitutions that is insensitive to α-conversion, and allows directly embedding the system into rewriting logic.