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
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)
Uses Software
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