Skip to content

Research at St Andrews

Coinductive soundness of corecursive type class resolution

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

Open Access permissions



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

School/Research organisations


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
StatePublished - 18 Aug 2016
EventInternational Symposium on Logic-based Program Synthesis and Transformation - University of Edinburgh, Edinburgh, United Kingdom
Duration: 6 Sep 20168 Sep 2016
Conference number: 26


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

    Research areas

  • Resolution, Coinduction, Herbrand models, Type classes

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: 245112479