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

František Farka, Ekaterina Komendantskya, Kevin Hammond

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
2 Downloads (Pure)

Abstract

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
Volume18
Issue number3-4
Early online date10 Aug 2018
DOIs
Publication statusPublished - 2018
Event34th International Conference on Logic Programming (ICLP 2018) - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018
Conference number: 34
https://www.cs.nmsu.edu/ALP/iclp2018/

Keywords

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

Fingerprint

Dive into the research topics of 'Proof-relevant Horn clauses for dependent type inference and term synthesis'. Together they form a unique fingerprint.

Cite this