A type-theoretic approach to resolution

Peng Fu (Lead / Corresponding author), Ekaterina Komendantskaya

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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
PublisherSpringer International Publishing
Number of pages16
ISBN (Electronic)9783319274362
ISBN (Print)9783319274355
Publication statusPublished - 2015
Event 25th International Symposium on Logic-Based Program Synthesis and Transformation - University of Siena, Siena, Italy
Duration: 13 Jul 201515 Jul 2015

Publication series

NameLecture notes in computer science
PublisherSpringer International Publishing
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference 25th International Symposium on Logic-Based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2015
Internet address


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

ASJC Scopus subject areas

  • General Computer Science
  • Theoretical Computer Science


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

Cite this