Coinductive soundness of corecursive type class resolution

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

Coinductive soundness of corecursive type class resolution

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)
Editors	Manuel V. Hermenegildo, Pedro Lopez-Garcia
Publisher	arXiv
Number of pages	15
Publication status	Published - 18 Aug 2016
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/

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	http://www.cliplab.org/Conferences/LOPSTR16/

Keywords

Resolution
Coinduction
Herbrand models
Type classes

Access to Document

paper
© 2016 the Authors. This work has been made available online with permission from the authors. This is the author created accepted version manuscript following peer review, and was originally published at: https://arxiv.org/abs/1608.05233
Accepted author manuscript, 427 KB

https://arxiv.org/abs/1608.05233

Handle.net

Persistent link

H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase
Hammond, K. (PI)
Joint Research Centre European Commission
1/04/15 → 31/03/18
Project: Standard

Coinductive soundness of corecursive type class resolution
Farka, F., Komendantskaya, E. & Hammond, K., 2017, Logic-Based Program Synthesis and Transformation: 26th International Symposium, LOPSTR 2016, Edinburgh, Scotland, UK, September 6-8, 2016. Revised Selected Papers. Hermenegildo, M. V. & Lopez-Garcia, P. (eds.). Cham: Springer, p. 311-327 (Lecture Notes in Computer Science (Theoretical Computer Science and General Issues); vol. 10184).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

Proof-relevant resolution - the foundations of constructive proof automation
Farka, F. (Author), Hammond, K. (Supervisor), 30 Jun 2021
Student thesis: Doctoral Thesis (PhD)

Cite this

@inproceedings{8a318703e2b14d7f8253328a0a836902,

title = "Coinductive soundness of corecursive type class resolution",

abstract = "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.",

keywords = "Resolution, Coinduction, Herbrand models, Type classes",

author = "Franti{\v s}ek Farka and Ekaterina Komendantskaya and Kevin Hammond and Peng Fu",

note = "This work has been partially supported by the EU Horizon 2020 grant “RePhrase: Refactoring Parallel Heterogeneous Resource-Aware Applications - a Software Engineering Approach” (ICT-644235), by COST Action IC1202 (TACLe), supported by COST (European Cooperation in Science and Technology), and by EPSRC grant EP/K031864/1-2 “{\textquoteleft}Coalgebraic Logic Programming for Type Inference”.; International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR 2016 ; Conference date: 06-09-2016 Through 08-09-2016",

year = "2016",

month = aug,

day = "18",

language = "English",

editor = "Hermenegildo, \{Manuel V.\} and Pedro Lopez-Garcia",

booktitle = "Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)",

publisher = "arXiv",

url = "http://www.cliplab.org/Conferences/LOPSTR16/",

}

Farka, F, Komendantskaya, E, Hammond, K & Fu, P 2016, Coinductive soundness of corecursive type class resolution. in MV Hermenegildo & P Lopez-Garcia (eds), Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). arXiv, International Symposium on Logic-based Program Synthesis and Transformation, Edinburgh, United Kingdom, 6/09/16. <https://arxiv.org/abs/1608.05233>

Coinductive soundness of corecursive type class resolution. / Farka, František; Komendantskaya, Ekaterina; Hammond, Kevin et al.
Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). ed. / Manuel V. Hermenegildo; Pedro Lopez-Garcia. arXiv, 2016.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Coinductive soundness of corecursive type class resolution

AU - Farka, František

AU - Komendantskaya, Ekaterina

AU - Hammond, Kevin

AU - Fu, Peng

N1 - Conference code: 26

PY - 2016/8/18

Y1 - 2016/8/18

N2 - 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.

AB - 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.

KW - Resolution

KW - Coinduction

KW - Herbrand models

KW - Type classes

M3 - Conference contribution

BT - Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)

A2 - Hermenegildo, Manuel V.

A2 - Lopez-Garcia, Pedro

PB - arXiv

T2 - International Symposium on Logic-based Program Synthesis and Transformation

Y2 - 6 September 2016 through 8 September 2016

ER -

Coinductive soundness of corecursive type class resolution

Abstract

Conference

Keywords

Access to Document

Handle.net

Fingerprint

Projects

H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase

Research output

Coinductive soundness of corecursive type class resolution

Student theses

Proof-relevant resolution - the foundations of constructive proof automation

Cite this