Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. Issue 3 (10th August 2018)

• Record Type: Journal Article
• Authors: FARKA, FRANTIŠEK; KOMENDANTSKYA, EKATERINA; HAMMOND, KEVIN
• Editors: Dal Palu, Alessandro; Tarau, Paul
• Is Part Of: Theory and practice of logic programming. Volume 18:Issue 3/4(2018)
• Page Start: 484
• Page End: 501
• Publication Date: 2018-08-10
• Subjects: Proof-relevant logic, -- Horn clauses, -- Dependent types, -- Type Inference, -- Proof-relevant resolution; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068418000212
• Languages: English
• ISSNs: 1471-0684

Abstract

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.