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

arXiv: https://arxiv.org/abs/1804.11250 · HTML: https://mlsanity.com/paper/1804.11250/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Apr 2018.

## Built on by (most cited first, 1 of 1)

- [When Agda met Vampire](https://mlsanity.com/paper/2602.18844/) (2026)

## Abstract (arXiv)

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 new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method. The paper is under consideration for acceptance in TPLP.