Skip to content

Research at St Andrews

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

Research output: Contribution to journalArticle

Open Access permissions


Open Access Status

  • Embargoed (until 10/02/19)



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
StatePublished - 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 author

  1. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  2. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V. Feb 2018 In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  3. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K. Jun 2017 In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

  4. Coinductive soundness of corecursive type class resolution

    Farka, F., Komendantskaya, E. & Hammond, K. 2017 Logic-Based Program Synthesis and Transformation: 26th International Symposium, LOPSTR 2016, Edinburgh, Scotland, UK, September 6-8, 2016. Revised Selected Papers. Hermenegildo, M. V. & Lopez-Garcia, P. (eds.). Cham: Springer, p. 311-327 (Lecture Notes in Computer Science (Theoretical Computer Science and General Issues); vol. 10184)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 journalArticle

ID: 255429602