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

DOI10.1017/S1471068418000212MaRDI QIDQ4559809zbMATHOpenAlexWikidataFDO

Authors František Farka, Ekaterina Komendantskya, Kevin Hammond

Publication date 4 December 2018

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.11250

zbMATH Keywords

dependent typesHorn clausestype inferenceproof-relevant resolutionproof-relevant logic

Mathematics Subject Classification ID

Logic programming (68N17) Mechanization of proofs and logical operations (03B35) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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. The paper is under consideration for acceptance in TPLP.

Recommendations

• Publication:4508310
• A type-theoretic approach to resolution
• scientific article; zbMATH DE number 1614692
• Auto in Agda. Programming proof search using reflection
• Higher-order unification with dependent function types

Cites work

• scientific article; zbMATH DE number 1158760 (Why is no real title available?)
• A theory of type polymorphism in programming
• An insider's look at LF type reconstruction: everything you (n)ever wanted to know
• An introduction to small scale reflection in Coq
• Automatically proving equivalence by type-safe reflection
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Coinductive soundness of corecursive type class resolution
• Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4--6, 2016. Proceedings
• HM(X) type inference is CLP(X) solving
• Idris, a general-purpose dependently typed programming language: Design and implementation
• On equivalence and canonical forms in the LF type theory
• Operational semantics of resolution and productivity in Horn clause logic
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

Cited in

(4)

• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Proof-term synthesis on dependent-type systems via explicit substitutions
• Proof relevant corecursive resolution
• scientific article; zbMATH DE number 1512625 (Why is no real title available?)

Describes a project that uses

Uses Software

• ML
• Beluga
• Coq/SSReflect
• Irdis
• Idris

This page was built for publication: Proof-relevant Horn clauses for dependent type inference and term synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559809)