Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

František Farka, Ekaterina Komendantskya, Kevin Hammond

First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a…