Projects per year
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 language | English |
---|---|
Title of host publication | Logic-Based Program Synthesis and Transformation |
Subtitle of host publication | 26th International Symposium, LOPSTR 2016, Edinburgh, Scotland, UK, September 6-8, 2016. Revised Selected Papers |
Editors | Manuel V Hermenegildo, Pedro Lopez-Garcia |
Place of Publication | Cham |
Publisher | Springer |
Pages | 311-327 |
ISBN (Electronic) | 9783319631394 |
ISBN (Print) | 9783319631387 |
DOIs | |
Publication status | Published - 2017 |
Event | International Symposium on Logic-based Program Synthesis and Transformation - University of Edinburgh, Edinburgh, United Kingdom Duration: 6 Sept 2016 → 8 Sept 2016 Conference number: 26 http://www.cliplab.org/Conferences/LOPSTR16/ |
Publication series
Name | Lecture Notes in Computer Science (Theoretical Computer Science and General Issues) |
---|---|
Publisher | Springer International Publishing |
Volume | 10184 |
ISSN (Print) | 0302-9743 |
Conference
Conference | International Symposium on Logic-based Program Synthesis and Transformation |
---|---|
Abbreviated title | LOPSTR 2016 |
Country/Territory | United Kingdom |
City | Edinburgh |
Period | 6/09/16 → 8/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.Projects
- 2 Finished
-
Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems
Thomson, J. D. (PI), Hammond, K. (CoI) & Sarkar, S. (CoI)
1/07/17 → 31/12/20
Project: Standard
-
H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase
Hammond, K. (PI)
1/04/15 → 31/03/18
Project: Standard
Research output
- 1 Conference contribution
-
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 proceeding › Conference contribution
Open AccessFile