A type-theoretic approach to resolution

Peng Fu (Lead / Corresponding author), Ekaterina Komendantskaya

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

3 Citations (Scopus)

Abstract

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
Pages91-106
Number of pages16
ISBN (Electronic)9783319274362
ISBN (Print)9783319274355
DOIs
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
http://alpha.diism.unisi.it/lopstr15/

Publication series

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

Conference

Conference 25th International Symposium on Logic-Based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2015
CountryItaly
CitySiena
Period13/07/1515/07/15
Internet address

Keywords

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

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

Cite this