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

DOI10.1017/S1471068418000212zbMATH Open1451.68323arXiv1804.11250OpenAlexW2964059082WikidataQ129410361 ScholiaQ129410361MaRDI QIDQ4559809FDOQ4559809

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)

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.

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

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

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)

Cites Work

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

Cited In (3)

• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Title not available (Why is that?)
• Proof-term synthesis on dependent-type systems via explicit substitutions

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)