A type-theoretic approach to resolution

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Citations (Scopus)


We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of program transformation that allows to transform logic programs in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers
EditorsMoreno Falaschi
Number of pages16
ISBN (Electronic)9783319274362
ISBN (Print)9783319274355
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


  • Logic programming
  • Typed lambda calculus
  • Realizability transformation
  • Reduction systems
  • Structural resolution


Dive into the research topics of 'A type-theoretic approach to resolution'. Together they form a unique fingerprint.

Cite this