Skip to main content
SpringerLink
Log in

Chapter 4. Basic Category Theory for Models of Syntax

  • Chapter
Generic Programming

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2793))

Abstract

A preliminary version of these notes formed the basis of four lectures given at the Summer School on Generic Programming, Oxford, UK, which took place during August 2002. The aims of the notes are to provide an introduction to very elementary category theory, and to show how such category theory can be used to provide both abstract and concrete mathematical models of syntax. Much of the material is now standard, but some of the ideas which are used in the modeling of syntax involving variable binding are quite new.

It is assumed that readers are familiar with elementary set theory and discrete mathematics, and have met formal accounts of the kinds of syntax as may be defined using the (recursive) datatype declarations that are common in modern functional programming languages. In particular, we assume readers know the basics of λ-calculus.

A pedagogical feature of these notes is that we only introduce the category theory required to present models of syntax, which are illustrated by example rather than through a general theory of syntax.

This work was supported by EPSRC grant number GR/M98555.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.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. Ambler, S.J., Crole, R.L., Momigliano, A.: Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, p. 13. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Blackhouse, R., Crole, R.L., Gibbons, J.: Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, p. 281. Springer, Heidelberg (2002)

    Google Scholar 

  3. Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (1985)

    MATH  Google Scholar 

  4. Barr, M., Wells, C.: Category Theory for Computing Science. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  5. Crole, R.L.: Categories for Types. Cambridge Mathematical Textbooks, pp. xvii+335. Cambridge University Press (1993) ISBN 0521450926HB, 0521457017PB

    Google Scholar 

  6. de Bruijn, N.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34(5), 381–392 (1972)

    Google Scholar 

  7. Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS (LNAI), vol. 902, pp. 124–138. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  8. Despeyroux, J., Pfenning, F., Schürmann, C.: Primitive recursion for higherorder abstract syntax. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 147–163. Springer, Heidelberg (1997)

    Google Scholar 

  9. Fiore, M., Plotkin, G.D., Turi, D.: Abstract Syntax and Variable Binding. In: Longo, G. (ed.) Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, pp. 193–202. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  10. Freyd, P.J., Scedrov, A.: Categories, Allegories. Elsevier Science Publishers, Amsterdam (1990); Appears as Volume 39 of the North-Holland Mathematical Library

    MATH  Google Scholar 

  11. Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: Longo, G. (ed.) Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, pp. 214–224. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  12. Gordon, A.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS (LNAI), vol. 780, Springer, Heidelberg (1994)

    Google Scholar 

  13. Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS (LNAI), vol. 1125, pp. 173–190. Springer, Heidelberg (1996)

    Google Scholar 

  14. Hofmann, M.: Semantical analysis for higher-order abstract syntax. In: Longo, G. (ed.) Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, pp. 204–213. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  15. Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 963–978. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Elsevier (1999)

    MATH  Google Scholar 

  17. Johnstone, P.T.: Topos Theory. Academic Press, London (1977)

    MATH  Google Scholar 

  18. Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  19. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1971)

    MATH  Google Scholar 

  20. Mac Lane, S.M., Moerdijk, I.: Topos theory. In: Hazewinkel, M. (ed.) Handbook of Algebra, vol. 1, pp. 501–528. North-Holland, Amsterdam (1996)

    Google Scholar 

  21. Mac Lane, M., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer, New York (1992)

    Google Scholar 

  22. McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Transaction in Computational Logic (2001) (to appear)

    Google Scholar 

  23. McKinna, J., Pollack, R.: Some Type Theory and Lambda Calculus Formalised. To appear in Journal of Automated Reasoning, Special Issue on Formalised Mathematical Theories (F. Pfenning (Ed.))

    Google Scholar 

  24. McLarty, C.: Elementary Categories, Elementary Toposes. Oxford Logic Guides, vol. 21. Oxford University Press, Oxford (1991)

    Google Scholar 

  25. Pfenning, F.: Computation and deduction. Lecture notes, vol. 277, Revised 1994. Cambridge University Press, Cambridge (1996)

    Google Scholar 

  26. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1988, pp. 199–208 (1988)

    Google Scholar 

  27. Pierce, B.C.: Basic Category Theory for Computer Scientists. Foundations of Computing Series. The MIT Press, Cambridge (1991)

    Google Scholar 

  28. Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS (LNAI), vol. 2215, pp. 219–242. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  29. Poigné, A.: Basic category theory. In: Handbook of Logic in Computer Science, vol. 1. Oxford University Press, Oxford (1992)

    Google Scholar 

  30. Smyth, M.B., Plotkin, G.D.: The Category Theoretic Solution of Recursive Domain Equations. SIAM Journal of Computing 11(4), 761–783 (1982)

    Google Scholar 

  31. Taylor, P.: Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics, vol. 59. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  32. Walters, R.F.C.: Categories and Computer Science. Cambridge Computer Science Texts, vol. 28. Cambridge University Press, Cambridge (1991)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Leicester, Leicester, LE1 7RH, UK

    R. L. Crole

Authors
  1. R. L. Crole
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

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

    Roland Backhouse

  2. Computing Laboratory, Oxford University,  

    Jeremy Gibbons

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Crole, R.L. (2003). Chapter 4. Basic Category Theory for Models of Syntax. In: Backhouse, R., Gibbons, J. (eds) Generic Programming. Lecture Notes in Computer Science, vol 2793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45191-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45191-4_4

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45191-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation