Skip to content

Research at St Andrews

Coinductive soundness of corecursive type class resolution

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


František Farka, Ekaterina Komendantskaya, Kevin Hammond

School/Research organisations


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
ISBN (Electronic)9783319631394
ISBN (Print)9783319631387
StatePublished - 2017
EventInternational Symposium on Logic-based Program Synthesis and Transformation - University of Edinburgh, Edinburgh, United Kingdom
Duration: 6 Sep 20168 Sep 2016
Conference number: 26

Publication series

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


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

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  2. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V. Feb 2018 In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  3. Proof-relevant Horn clauses for dependent type inference and term synthesis

    Farka, F., Komendantskya, E. & Hammond, K. 2018 In : Theory and Practice of Logic Programming. 18, 3-4, p. 484-501

    Research output: Contribution to journalArticle

  4. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K. Jun 2017 In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

ID: 250119584