Coinductive soundness of corecursive type class resolution

František Farka, Ekaterina Komendantskaya, Kevin Hammond

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

Abstract

Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.
Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication26th International Symposium, LOPSTR 2016, Edinburgh, Scotland, UK, September 6-8, 2016. Revised Selected Papers
EditorsManuel V Hermenegildo, Pedro Lopez-Garcia
Place of PublicationCham
PublisherSpringer
Pages311-327
ISBN (Electronic)9783319631394
ISBN (Print)9783319631387
DOIs
Publication statusPublished - 2017
EventInternational Symposium on Logic-based Program Synthesis and Transformation - University of Edinburgh, Edinburgh, United Kingdom
Duration: 6 Sept 20168 Sept 2016
Conference number: 26
http://www.cliplab.org/Conferences/LOPSTR16/

Publication series

NameLecture Notes in Computer Science (Theoretical Computer Science and General Issues)
PublisherSpringer International Publishing
Volume10184
ISSN (Print)0302-9743

Conference

ConferenceInternational Symposium on Logic-based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2016
Country/TerritoryUnited Kingdom
CityEdinburgh
Period6/09/168/09/16
Internet address

Keywords

  • Resolution
  • Coinduction
  • Herbrand models
  • Type classes
  • Haskell
  • Horn clauses

Fingerprint

Dive into the research topics of 'Coinductive soundness of corecursive type class resolution'. Together they form a unique fingerprint.
  • Coinductive soundness of corecursive type class resolution

    Farka, F., Komendantskaya, E., Hammond, K. & Fu, P., 18 Aug 2016, Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). Hermenegildo, M. V. & Lopez-Garcia, P. (eds.). arXiv, 15 p.

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

    Open Access
    File

Cite this