Projects per year
Abstract
Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have welldefined inductive meaning, whereas some nonterminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the rôle of coinductive hypothesis. This paper introduces a heuristic method for obtaining richer coinductive hypotheses in the form of Horn formulas. Our approach subsumes cycle detection and gives coinductive meaning to a larger class of derivations. For this purpose we extend resolution with Horn formula resolvents and corecursive evidence generation. We illustrate our method on nonterminating type class resolution problems.
Original language  English 

Title of host publication  FLOPS 2016 
Subtitle of host publication  Functional and Logic Programming 
Editors  Oleg Kiselyov, Andy King 
Place of Publication  Switzerland 
Publisher  Springer Verlag 
Pages  126143 
Number of pages  18 
ISBN (Electronic)  9783319296043 
ISBN (Print)  9783319296036 
DOIs  
Publication status  Published  2016 
Event  13th International Symposium on Functional and Logic Programming, FLOPS 2016  Kochi, Japan Duration: 4 Mar 2016 → 6 Mar 2016 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer Verlag 
Volume  9613 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Conference
Conference  13th International Symposium on Functional and Logic Programming, FLOPS 2016 

Country/Territory  Japan 
City  Kochi 
Period  4/03/16 → 6/03/16 
Keywords
 Coinductive proofs
 Corecursion
 Haskell type class inference
 Horn clause logic
 Resolution
Fingerprint
Dive into the research topics of 'Proof relevant corecursive resolution'. Together they form a unique fingerprint.Projects
 1 Finished

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)
Komendantskaya, E.
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research