Skip to content

Research at St Andrews

Proof-relevant Horn clauses for dependent type inference and term synthesis

Research output: Contribution to journalArticlepeer-review

Open Access permissions



František Farka, Ekaterina Komendantskya, Kevin Hammond

School/Research organisations


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.


Original languageEnglish
Pages (from-to)484-501
JournalTheory and Practice of Logic Programming
Issue number3-4
Early online date10 Aug 2018
Publication statusPublished - 2018
Event34th International Conference on Logic Programming (ICLP 2018) - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018
Conference number: 34

    Research areas

  • Proof-relevant logic, Horn clauses, Dependent types, Type Inference, Proof-relevant resolution

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by journal

  1. A review of literature on parallel constraint solving

    Gent, I. P., Miguel, I. J., Nightingale, P. W., McCreesh, C., Prosser, P., Moore, N. & Unsworth, C., Sep 2018, In: Theory and Practice of Logic Programming. 18, 5-6, p. 725-758 34 p.

    Research output: Contribution to journalArticlepeer-review

ID: 255429602