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

作     者：Farka, Frantisek Komendantskya, Ekaterina Hammond, Kevin 

作者机构：Univ St Andrews St Andrews Fife Scotland Heriot Watt Univ Edinburgh Midlothian Scotland 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 (逻辑程序设计理论与实践)

年 卷 期：2018年第18卷第3-4期

页      面：484-501页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：EPSRC grant "Coalgebraic Logic Programming for Type Inference" [EP/K031864/1-2] EU Horizon 2020 grant "RePhrase: Refactoring Parallel Heterogeneous Resource-Aware Applications - a Software Engineering Approach" [ICT-644235] COST Action [IC1202] COST (European Cooperation in Science and Technology) EPSRC [EP/K031864/1, EP/P020631/1, EP/K031864/2, EP/N014758/1] Funding Source: UKRI 

主　　题：Proof-relevant logic Horn clauses Dependent types Type Inference Proof-relevant resolution 

摘      要：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.