Skip to main content
SpringerLink
Log in

Datatype-Generic Reasoning

  • Conference paper
Logical Approaches to Computational Barriers (CiE 2006)

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

Included in the following conference series:

  • 949 Accesses

Abstract

Datatype-generic programs are programs that are parameterised by a datatype. Designing datatype-generic programs brings new challenges and new opportunities. We review the allegorical foundations of a methodology of designing datatype-generic programs. The effectiveness of the methodology is demonstrated by an extraordinarily concise proof of the well-foundedness of a datatype-generic occurs-in relation.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Jeuring, J., Jansson, P.: Polytypic programming. In: Launchbury, J., Sheard, T., Meijer, E. (eds.) AFP 1996. LNCS, vol. 1129, pp. 68–114. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  2. Hinze, R.: Polytypic values possess polykinded types. Science of Computer Programming 43(2-3), 129–159 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  3. Hinze, R., Jeuring, J., Löh, A.: Type-indexed data types. Science of Computer Programming 51(1-2), 117–151 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  4. Löh, A., Clarke, D., Jeuring, J.: Dependency-style Generic Haskell. In: Shivers, O. (ed.) Proceedings of the International Conference, ICFP 2003, pp. 141–152. ACM Press, New York (2003)

    Google Scholar 

  5. Doornbos, H., Backhouse, R.: Induction and recursion on datatypes. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 242–256. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  6. Doornbos, H.: Reductivity arguments and program construction. PhD thesis, Eindhoven University of Technology, Department of Mathematics and Computing Science (1996)

    Google Scholar 

  7. Doornbos, H., Backhouse, R.: Reductivity. Science of Computer Programming 26(1-3), 217–236 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  8. Jansson, P., Jeuring, J.: Functional pearl: Polytypic unification. Journal of Functional Programming (1998)

    Google Scholar 

  9. Backhouse, R., Jansson, P., Jeuring, J., Meertens, L.: Generic programming. An introduction. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol. 1608, pp. 28–115. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Hoare, C., He, J.: The weakest prespecification. Fundamenta Informaticae 9, 51–84 (1986)

    MathSciNet  MATH  Google Scholar 

  11. Freyd, P., Ščedrov, A.: Categories, Allegories. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  12. Backhouse, R.: Naturality of homomorphisms. Lecture notes, International Summer School on Constructive Algorithmics, vol. 3 (1989)

    Google Scholar 

  13. Backhouse, R., Bruin, P.d., Malcolm, G., Voermans, T., Woude, J.v.d.: Relational catamorphisms. In: Möller, B. (ed.) Proceedings of the IFIP TC2/WG2.1 Working Conference on Constructing Programs from Specifications, pp. 287–318. Elsevier Science Publishers B.V., Amsterdam (1991)

    Google Scholar 

  14. Backhouse, R., Woude, J.v.d.: Demonic operators and monotype factors. Mathematical Structures in Computer Science 3(4), 417–433 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  15. Bird, R.S., de Moor, O.: Algebra of Programming. Prentice-Hall International, Englewood Cliffs (1996)

    Book  MATH  Google Scholar 

  16. Backhouse, R., Bruin, P.d., Hoogendijk, P., Malcolm, G., Voermans, T., Woude, J.v.d.: Polynomial relators. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST 1991, Workshops in Computing, pp. 303–326. Springer, Heidelberg (1992)

    Google Scholar 

  17. Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R. (ed.) IFIP 1983, pp. 513–523. Elsevier Science Publishers, Amsterdam (1983)

    Google Scholar 

  18. Wadler, P.: Theorems for free! In: 4’th Symposium on Functional Programming Languages and Computer Architecture. ACM, London (1989)

    Google Scholar 

  19. Hoogendijk, P.: A Generic Theory of Datatypes. PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology (1997)

    Google Scholar 

  20. Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 124–144. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  21. Meijer, E.: Calculating Compilers. PhD thesis, University of Nijmegen (1992)

    Google Scholar 

  22. Backhouse, R., Doornbos, H.: Mathematics of recursive program construction (2001), Internet publication, Available from: http://www.cs.nott.ac.uk/~rcb/MPC/papers

  23. Malcolm, G.: Algebraic data types and program transformation. PhD thesis, Groningen University (1990)

    Google Scholar 

  24. Malcolm, G.: Data structures and program transformation. Science of Computer Programming 14(2-3), 255–280 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  25. Backhouse, R., Hoogendijk, P.: Final dialgebras: From categories to allegories. Theoretical Informatics and Applications 33(4/5), 401–426 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  26. Hoogendijk, P., de Moor, O.: Container types categorically. Journal of Functional Programming 10(2), 191–225 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  27. Doornbos, H., Backhouse, R.C., van der Woude, J.: A calculation approach to mathematical induction. Theoretical Computer Science 179, 103–135 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  28. Jansson, P., Jeuring, J.: PolyP - a polytypic programming language extension. In: POPL 1997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 470–482. ACM Press, New York (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Information Technology, University of Nottingham, Nottingham, NG8 1BB, England

    Roland Backhouse

Authors
  1. Roland Backhouse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Swansea, United Kingdom

    Arnold Beckmann

  2. Department of Computer Science, University of Wales Swansea, Singleton Park, SA2 8PP, Swansea, UK

    Ulrich Berger

  3. Universiteit van Amsterdam, Plantage Muidergracht 24, 1018, Amsterdam, TV, The Netherlands

    Benedikt Löwe

  4. School of Physical Sciences, Swansea University, Singleton Park, SA2 8PP, Swansea, Wales, United Kingdom

    John V. Tucker

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Backhouse, R. (2006). Datatype-Generic Reasoning. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds) Logical Approaches to Computational Barriers. CiE 2006. Lecture Notes in Computer Science, vol 3988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780342_3

Download citation

  • DOI: https://doi.org/10.1007/11780342_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35466-6

  • Online ISBN: 978-3-540-35468-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation