Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Logic-Based Program Synthesis and Transformation

LOPSTR 2016: Logic-Based Program Synthesis and Transformation pp 311–327Cite as

Coinductive Soundness of Corecursive Type Class Resolution

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10184))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Colmerauer, A.: Equations and inequations on finite and infinite trees. In: FGCS, pp. 85–99 (1984)

    Google Scholar 

  2. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Proving correctness of imperative programs by linearizing constrained horn clauses. TPLP 15(4–5), 635–650 (2015)

    MathSciNet  Google Scholar 

  3. Devriese, D., Piessens, F.: On the bright side of type classes: instance arguments in Agda. In: Proceedings of ICFP 2011, Tokyo, 19–21 September 2011, pp. 143–155 (2011)

    Google Scholar 

  4. Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in Horn clause logic. Form. Asp. Comput. 29, 453–474 (2017). doi:10.1007/s00165-016-0403-1

  5. Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126–143. Springer, Cham (2016). doi:10.1007/978-3-319-29604-3_9

    Chapter  Google Scholar 

  6. Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: Proceedings of ICFP 2011, Tokyo, 19–21 September 2011, pp. 163–175 (2011)

    Google Scholar 

  7. Hall, C.V., Hammond, K., Jones, S.L.P., Wadler, P.: Type classes in Haskell. ACM Trans. Program. Lang. Syst. 18(2), 109–138 (1996)

    Article  Google Scholar 

  8. Howard, W.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pp. 479–490. Academic Press, New York (1980)

    Google Scholar 

  9. Jaffar, J., Stuckey, P.J.: Semantics of infinite tree logic programming. Theor. Comput. Sci. 46(3), 141–158 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  10. Komendantskaya, E., Li T.: Productive corecursion in logic programming. In: Proceedings of ICLP 2017. TPLP (to appear, 2017)

    Google Scholar 

  11. Lämmel, R., Peyton Jones, S.L.: Scrap your boilerplate with class: extensible generic functions. In: Proceedings of ICFP 2005, Tallinn, 26–28 September 2005, pp. 204–215 (2005)

    Google Scholar 

  12. Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)

    Book  MATH  Google Scholar 

  13. Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4), 15:1–15:41 (2009)

    Article  MATH  Google Scholar 

  14. Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73420-8_42

    Chapter  Google Scholar 

  15. Stuckey, P.J., Sulzmann, M.: A theory of overloading. ACM Trans. Program. Lang. Syst. 27(6), 1216–1269 (2005)

    Article  MATH  Google Scholar 

  16. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of POPL 1989, pp. 60–76. ACM, New York (1989)

    Google Scholar 

Download references

Acknowledgements

This work has been supported by the EPSRC grant “Coalgebraic Logic Programming for Type Inference” EP/K031864/1-2, EU Horizon 2020 grant “RePhrase: Refactoring Parallel Heterogeneous Resource-Aware Applications - a Software Engineering Approach” (ICT-644235), and by COST Action IC1202 (TACLe), supported by COST (European Cooperation in Science and Technology).

Author information

Authors and Affiliations

  1. University of St Andrews, St Andrews, Scotland

    František Farka & Kevin Hammond

  2. Heriot-Watt University, Edinburgh, Scotland

    František Farka & Ekaterina Komendantskaya

Authors
  1. František Farka
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ekaterina Komendantskaya
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kevin Hammond
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to František Farka .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute and Universidad Politécnica de Madrid, Madrid, Spain

    Manuel V Hermenegildo

  2. IMDEA Software Institute and CSIC, Madrid, Spain

    Pedro Lopez-Garcia

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Farka, F., Komendantskaya, E., Hammond, K. (2017). Coinductive Soundness of Corecursive Type Class Resolution. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63139-4_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63138-7

  • Online ISBN: 978-3-319-63139-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation