Skip to main content
SpringerLink
Log in

Category theory and programming language semantics: An overview

  • Part II Research Contributions
  • Chapter
  • First Online:
Category Theory and Computer Programming

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

Abstract

I have not tried to be comprehensive here. Instead I have tried to pursue the idea of category theory as a kind of type theory and thereby I have only included those uses of category theory which I have found particularly useful for understanding type theory, domain theory and algebraic semantics. Therefore, several things have been excluded, such as Arbib and Manes' (1980) partially additive semantics and Winskel's (1984) categories of Petri nets, to mention only two examples of interest.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • S. Abramsky, Some dichotomies in programming theory, notes, in P. Dybjer, B. Nordström, K. Petersson and J. Smith, eds., Proceedings of the Workshop on Specification and Derivation of Programs, Marstrand, Sweden, June 1985, Report, Programming Methodology Group, Göteborg (to appear).

    Google Scholar 

  • P. Aczel, A note on Scott's theory of domains, unpublished note, Department of Mathematics, University of Manchester, 1983.

    Google Scholar 

  • ADJ (J.A. Goguen, J.W. Thatcher, E.G. Wagner, J.B. Wright), A Junction Between Computer Science and Category Theory, I: Basic Concepts and Examples, IBM T.J. Watson Research Center Technical Report RC 4526, September 1973.

    Google Scholar 

  • ADJ (J.B. Wright, J.A. Goguen, J.W. Thatcher, E.G. Wagner), Rational algebraic theories and fixed point solutions, in Proceedings 17th IEEE Symposium on Foundations of Computer Science, Houston, Texas (1976).

    Google Scholar 

  • ADJ (J.A. Goguen, J.W. Thatcher, E.G. Wagner, J.B. Wright), Initial algebra semantics and continuous algebras, J.ACM 24, 1 (1977) 68–95.

    Google Scholar 

  • ADJ (J.A. Goguen, J.W. Thatcher, E.G. Wagner), An initial algebra approach to the specification, correctness and implementation of abstract data types, in R. Yeh, ed., Current Trends in Programming Methodology (Prentice-Hall, 1978) 80–149.

    Google Scholar 

  • ADJ (J.W. Thatcher, E.G. Wagner, J.B. Wright), More on advice on structuring compilers and proving them correct, Theoretical Computer Science 15 (1981) 223–249.

    Google Scholar 

  • M.A. Arbib and E.G. Manes, Arrows, Structures and Functors (Academic Press, 1975).

    Google Scholar 

  • M.A. Arbib and E.G. Manes, Partially additive categories and flow-diagram semantics, Journal of Algebra 62, 1 (1980).

    Google Scholar 

  • H.P. Barendregt, The Lambda Calculus. Its Syntax and Semantics (North-Holland, 1980); revised edition (North-Holland, 1984).

    Google Scholar 

  • G. Berry and P.L. Curien, Sequential algorithms on concrete data structures, Theoretical Computer Science 20 (1982) 265–321.

    Google Scholar 

  • R.M. Burstall and P.J. Landin, Programs and their proofs: an algebraic approach, in B. Meltzer and D. Michie, eds., Machine Intelligence 4 (Edinburgh University Press, 1969) 17–44.

    Google Scholar 

  • R.M. Burstall and J.W. Thatcher, The algebraic theory of recursive program schemes, in Category Theory Applied to Computation and control, LNCS 25 (Springer-Verlag, 1974) 126–131.

    Google Scholar 

  • J. Cartmell, Generalised algebraic theories and contextual categories, Ph.D. thesis, University of Oxford, 1978.

    Google Scholar 

  • P. Dybjer, Category-theoretic logics and algebras of programs, Ph.D. thesis, Chalmers University of Technology, 1983.

    Google Scholar 

  • P. Dybjer, Domain algebras, in J. Paredaens, ed., Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, LNCS 172 (Springer-Verlag, 1984) 138–150.

    Google Scholar 

  • P. Dybjer, Using domain algebras to prove the correctness of a compiler, in K. Mehlhorn, ed., STACS 85, Saarbrucken, Germany, LNCS 182 (Springer-Verlag, 1985) 98–108.

    Google Scholar 

  • C.C. Elgot, Algebraic theories and program schemes, in E. Engeler, ed., Symposium on Semantics of Algorithmic Languages. LNM 188 (Springer-Verlag, 1971) 71–88.

    Google Scholar 

  • C.C. Elgot, Monadic computation and iterative algebraic theories, in Logic Colloquium '73, Bristol, England (North-Holland, 1975) 175–230.

    Google Scholar 

  • J.A. Goguen and R.M. Burstall, Some fundamental tools for the semantics of computation; part 1: comma categories, colimits, signatures and theories, Theoretical Computer Science 31 (1984) 175–209.

    Google Scholar 

  • R. Goldblatt, Topoi — The Categorial Analysis of Logic (North-Holland, 1979).

    Google Scholar 

  • C.A. Gunter, Profinite solutions for recursive domain equations, Ph.D. thesis, Carnegie-Mellon University, 1985.

    Google Scholar 

  • M.C.B. Hennessy and G.D. Plotkin, Full abstraction for a simple parallel programming language, in J. Becvar, ed., MFCS 1979, LNCS 74 (Springer-Verlag, 1979) 108–120.

    Google Scholar 

  • H. Huwig and A. Poigne, A note on inconsistencies caused by fixpoints in a cartesian closed category, manuscript, Department of Computing, Imperial College, London, 1986.

    Google Scholar 

  • K. Karlsson and K. Petersson, eds., Workshop on Semantics of Programming Languages, Abstracts and Notes, Report, Programming Methodology Group, Göteborg, 1983.

    Google Scholar 

  • J. Lambek, Deductive systems and categories II, LNM 86 (Springer-Verlag, 1969) 76–122.

    Google Scholar 

  • J. Lambek, From λ-calculus to cartesian closed categories, in J.R. Hindley and J.P. Seldin, eds., To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism (Academic Press, 1980) 375–402.

    Google Scholar 

  • J. Lambek and P.J. Scott, Cartesian closed categories and λ-calculus, preprint, Department of Mathematics, McGill University, Montreal, 1983.

    Google Scholar 

  • F.W. Lawvere, Diagonal arguments and cartesian closed categories, in Category Theory, Homology Theory and their Applications II, LNM 92 (Springer-Verlag, 1969).

    Google Scholar 

  • D.J. Lehmann, On the algebra of order, Journal of Computer and System Sciences 21 (1980).

    Google Scholar 

  • D.J. Lehmann and M.B. Smyth, Data types (extended abstract), in Proceedings 18th IEEE Symposium on Foundations of Computer Science (1977) 7–12.

    Google Scholar 

  • D.J. Lehmann and M.B. Smyth, Algebraic specification of data types: a synthetic approach, Mathematical Systems Theory 14 (1981) 97–139.

    Google Scholar 

  • G. Longo and E. Moggi, Cartesian closed categories of enumerations for effective type structures, in G. Kahn, D.B. MacQueen and G. Plotkin, eds., Semantics of Data Types, International Symposium, Sophia-Antipolis, France, LNCS 173 (Springer-Verlag, 1984) 235–256.

    Google Scholar 

  • S. MacLane, Categories for the Working Mathematican (Springer-Verlag, 1971).

    Google Scholar 

  • P. Martin-Löf, Constructive mathematics and computer programming, in L.J. Cohen, J. Los, H. Pfeiffer and K.-P. Podewski, eds., Logic, Methodology and Philosophy of Science VI (North-Holland, 1982).

    Google Scholar 

  • P. Martin-Löf, The domain interpretation of type theory, notes, in Karlsson and Petersson (1983).

    Google Scholar 

  • P. Martin-Löf, Intuitionistic type theory (Bibliopolis, 1984).

    Google Scholar 

  • R. Milner, L. Morris, M. Newey, A logic for computable functions with reflexive and polymorphic types, in Proceedings of the Conference on Proving and Improving Programs, Arc-et-Senans, France, 1975.

    Google Scholar 

  • F.L. Morris, Advice on structuring compilers and proving them correct, in Conference Record of the ACM Symposium on Principles of Programming Languages, Boston (1973) 144–152.

    Google Scholar 

  • P. Mosses, A constructive approach to compiler correctness, in J.W. de Bakker and J. van Leeuwen, eds., Automata, Languages and Programming, 7th Colloquium, LNCS 85 (Springer-Verlag, 1980).

    Google Scholar 

  • K. Parsaye-Ghomi, Higher order abstract data types, Ph.D. thesis, UCLA, 1982.

    Google Scholar 

  • G.D. Plotkin, A powerdomain construction, SIAM Journal of Computing 5 (1976) 452–487.

    Google Scholar 

  • G.D. Plotkin, Domains, lecture notes, Department of Computer Science, University of Edinburgh, 1980.

    Google Scholar 

  • G.D. Plotkin, Types and partial functions, manuscript, Department of Computer Science, University of Edinburgh, 1984.

    Google Scholar 

  • A. Poigne, On semantic algebras: higher order structures, manuscript, Informatik II, Universität Dortmund, 1983.

    Google Scholar 

  • D.S. Scott, Continuous lattices, in F.W. Lawvere, ed., Toposes, Algebraic Geometry and Logic, LNM 274 (Springer-Verlag, 1972) 97–136.

    Google Scholar 

  • D.S. Scott, Some philosophical issues concerning theories of combinators, in C. Böhm, ed., λ-calculus and Computer Science Theory, Proceedings of the Symposium, LNCS 37 (Springer-Verlag, 1975) 346–366.

    Google Scholar 

  • D.S. Scott, Data types as lattices, SIAM Journal of Computing 5 (1976) 522–587.

    Google Scholar 

  • D.S. Scott, Relating theories of the λ-calculus, in J.R. Hindley and J.P. Seldin, eds., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, 1980) 403–450.

    Google Scholar 

  • D.S. Scott, A mathematical theory of computation, Technical Report, PRG-10, Oxford University Computing Laboratory, 1981.

    Google Scholar 

  • D.S. Scott, Domains for denotational semantics, in M. Nielson and E.M. Schmidt, eds., Automata, Languages and Programming, 9th Colloquium, Aarhus, LNCS 140 (Springer-Verlag, 1982) 577–613.

    Google Scholar 

  • M.B. Smyth, Effectively given domains, Theoretical Computer Science 5 (1977) 257–274.

    Google Scholar 

  • M.B. Smyth, Power domains, Journal of Computer and System Sciences 16 (1978) 23–36.

    Google Scholar 

  • M.B. Smyth, Power domains and predicate transformers: a topological view, in J. Diaz, ed., Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, LNCS 154 (Springer-Verlag, 1983 a) 662–676

    Google Scholar 

  • M.B. Smyth, The largest cartesian closed category of domains, Theoretical Computer Science 27 (1983 b) 109–119.

    Google Scholar 

  • M.B. Smyth and G.D. Plotkin, The category-theoretic solution of recursive domain equations, SIAM Journal of Computing 11 (1982) 761–783.

    Google Scholar 

  • M. Wand, On recursive specification of data types, in E.G. Manes, ed., Category Theory Applied to Computation and Control, LNCS 25 (Springer-Verlag, 1974).

    Google Scholar 

  • G. Winskel, A new definition of morphisms on Petri nets, in M. Fontet and K. Mehlhorn, eds., STACS 84, LNCS 166 (Springer-Verlag, 1984) 274–286.

    Google Scholar 

  • G. Winskel and K.G. Larsen, Using information systems to solve recursive domain equations effectively; in G. Kahn, D.B. MacQueen, G. Plotkin, eds., Semantics of Data Types, International Symposium, Sophia-Antipolis, France, LNCS 173 (Springer-Verlag, 1984) 109–130.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Methodology Group Department of Computer Sciences, Chalmers University of Technology and University of Göteborg, S-412 96, Göteborg, Sweden

    Peter Dybjer

Authors
  1. Peter Dybjer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

David Pitt Samson Abramsky Axel Poigné David Rydeheard

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Dybjer, P. (1986). Category theory and programming language semantics: An overview. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds) Category Theory and Computer Programming. Lecture Notes in Computer Science, vol 240. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17162-2_121

Download citation

  • DOI: https://doi.org/10.1007/3-540-17162-2_121

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-17162-1

  • Online ISBN: 978-3-540-47213-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation