Coinductive soundness of corecursive type class resolution

František Farka, Ekaterina Komendantskaya, Kevin Hammond, Peng Fu

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


Horn clauses and first-order resolution are commonly used for the implementation of type classes in Haskell. Recently, several core- cursive extensions to type class resolution have been proposed, with the common goal of allowing (co)recursive dictionary construction for those cases when resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its recent 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.
Original languageEnglish
Title of host publicationPre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)
EditorsManuel V. Hermenegildo, Pedro Lopez-Garcia
Number of pages15
Publication statusPublished - 18 Aug 2016
EventInternational Symposium on Logic-based Program Synthesis and Transformation - University of Edinburgh, Edinburgh, United Kingdom
Duration: 6 Sept 20168 Sept 2016
Conference number: 26


ConferenceInternational Symposium on Logic-based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2016
Country/TerritoryUnited Kingdom
Internet address


  • Resolution
  • Coinduction
  • Herbrand models
  • Type classes


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

Cite this