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

František Farka; Ekaterina Komendantskya; Kevin Hammond

doi:10.1017/S1471068418000212

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

František Farka, Ekaterina Komendantskya, Kevin Hammond

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

6 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 language	English
Pages (from-to)	484-501
Journal	Theory and Practice of Logic Programming
Volume	18
Issue number	3-4
Early online date	10 Aug 2018
DOIs	https://doi.org/10.1017/S1471068418000212
Publication status	Published - 2018
Event	34th International Conference on Logic Programming (ICLP 2018) - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 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

Access to Document

10.1017/S1471068418000212

Farka-2018-Proof-relevant-TPLP-AAM
© 2018, Cambridge University Press. This work has been made available online in accordance with the publisher’s policies. This is the author created accepted version manuscript following peer review and as such may differ slightly from the final published version. The final published version of this work is available at https://doi.org/10.1017/S1471068418000212
Accepted author manuscript, 592 KB

https://arxiv.org/abs/1804.11250

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems
Thomson, J. D. (PI), Hammond, K. (CoI) & Sarkar, S. (CoI)
EPSRC
1/07/17 → 31/12/20
Project: Standard
H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase
Hammond, K. (PI)
European Commission
1/04/15 → 31/03/18
Project: Standard

Slepice
Farka, F. (Creator), Komendantskya, E. (Creator) & Hammond, K. (Creator), GitHub, 17 Apr 2018
https://github.com/frantisekfarka/slepice
Dataset

Cite this

@article{2bfc140cb0714cd789bf3fb9b89bc1ce,

title = "Proof-relevant Horn clauses for dependent type inference and term synthesis",

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.",

keywords = "Proof-relevant logic, Horn clauses, Dependent types, Type Inference, Proof-relevant resolution",

author = "Franti{\v s}ek Farka and Ekaterina Komendantskya and Kevin Hammond",

note = "This work has been supported by the 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), and by COST Action IC1202 (TACLe), supported by COST (European Cooperation in Science and Technology).; 34th International Conference on Logic Programming (ICLP 2018), ICLP ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

doi = "10.1017/S1471068418000212",

language = "English",

volume = "18",

pages = "484--501",

journal = "Theory and Practice of Logic Programming",

issn = "1471-0684",

publisher = "Cambridge University Press",

number = "3-4",

url = "https://www.cs.nmsu.edu/ALP/iclp2018/",

}

TY - JOUR

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

AU - Farka, František

AU - Komendantskya, Ekaterina

AU - Hammond, Kevin

N1 - Conference code: 34

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Proof-relevant logic

KW - Horn clauses

KW - Dependent types

KW - Type Inference

KW - Proof-relevant resolution

U2 - 10.1017/S1471068418000212

DO - 10.1017/S1471068418000212

M3 - Article

SN - 1471-0684

VL - 18

SP - 484

EP - 501

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

IS - 3-4

T2 - 34th International Conference on Logic Programming (ICLP 2018)

Y2 - 14 July 2018 through 17 July 2018

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Projects

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems

H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase

Datasets

Slepice

Cite this