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

DOI10.1017/S1471068418000212zbMath1451.68323arXiv1804.11250OpenAlexW2964059082WikidataQ129410361 ScholiaQ129410361MaRDI QIDQ4559809

František Farka, Kevin Hammond, Ekaterina Komendantskya

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

Horn clausesdependent typestype inferenceproof-relevant resolutionproof-relevant logic

Mathematics Subject Classification ID

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

Related Items (1)

\texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• A theory of type polymorphism in programming
• Automatically proving equivalence by type-safe reflection
• 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
• On equivalence and canonical forms in the LF type theory
• Idris, a general-purpose dependently typed programming language: Design and implementation
• HM(X) type inference is CLP(X) solving
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4--6, 2016. Proceedings

This page was built for publication: Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis