[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

A proposed categorical semantics for Pure ML

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1992)

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

Included in the following conference series:

Abstract

This paper outlines an approach to modelling the purely functional fragment of ML: it concentrates on the semantics of the Modules system. Our proposed semantics is set-theoretic: types and values are modelled by sets and functions in a topos, a categorical model of constructive set theory. Synthetic domain theory allows us to make sense of fixed points and recursive domains in a set-theoretic setting, while the notions of classifying topos and ‘generic’ structure provide a useful way of interpreting signatures, functors and sharing, as well as Extended ML specifications. We only give an informal account, concentrating on motivation and examples rather than giving a rigorous formal development—only elementary category theory is used.

Research supported by SERC grant GR/F 31199, ‘Formal System Design’; the first author was also supported by an 1851 Research Fellowship

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.

Similar content being viewed by others

References

  1. P. Freyd, P. Mulry, G. Rosolini, D. S. Scott: Extensional PERs, in: Proc. of 5th Annual Symposium on Logic in Computer Science, 1990.

    Google Scholar 

  2. R. Harper, R. Milner, M. Tofte: A type discipline for program modules, in: Proc. of TAPSOFT '87, Springer LNCS 250, 1987.

    Google Scholar 

  3. R. Harper, J. Mitchell, E. Moggi: Higher-order modules and the phase distinction, in: Proc. 17th ACM Symposium on Principles of Programming Languages, 1990.

    Google Scholar 

  4. J. M. E. Hyland: The effective topos, in: The L. E. J. Brouwer Centenary Symposium (ed. A. S. Troelstra, D. van Dalen), North-Holland, 1982.

    Google Scholar 

  5. J. M. E. Hyland, E. P. Robinson, G. Rosolini: The discrete objects in the effective topos, Proc. Lond. Math. Soc. (3) 60 (1990) 1–36.

    Google Scholar 

  6. P. T. Johnstone: Topos Theory, Academic Press, 1977.

    Google Scholar 

  7. E. Kazmierczak: An institution for Extended ML, talk at the 9th Workshop on Abstract Data Types; report, in preparation.

    Google Scholar 

  8. J. Lambek, P. J. Scott: Introduction to Higher-Order Categorical Logic, Cambridge University Press, 1986.

    Google Scholar 

  9. D. MacQueen: Modules for Standard ML, in: Standard ML (R. Harper, D. MacQueen, R. Milner), available as ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science, University of Edinburgh.

    Google Scholar 

  10. D. MacQueen: Using dependent types to express modular structure, in: Proc. 13th ACM Symposium on Principles of Programming Languages, 1990.

    Google Scholar 

  11. R. Milner, M. Tofte: Commentary on Standard ML, MIT Press, 1990.

    Google Scholar 

  12. R. Milner, M. Tofte, R. Harper: The Definition of Standard ML, MIT Press, 1990.

    Google Scholar 

  13. J. Mitchell, R. Harper: The essence of ML, in: Proc. 15th ACM Symposium on Principles of Programming Languages, 1988.

    Google Scholar 

  14. J. Mitchell, G. D. Plotkin: Abstract data types have existential types, ACM Trans. Programming Languages and Systems, 10(3):470–502.

    Google Scholar 

  15. W. K.-S. Phoa: Effective domains and intrinsic structure, in: Proc. of 5th Annual Symposium on Logic in Computer Science, 1990.

    Google Scholar 

  16. W. K.-S. Phoa: Domain Theory in Realizability Toposes, dissertation, University of Cambridge, November 1990; available as CST-82-91/ECS-LFCS-91-171, Department of Computer Science, University of Edinburgh.

    Google Scholar 

  17. W. K.-S. Phoa: A simple categorical model of first-order polymorphism, submitted.

    Google Scholar 

  18. G. Rosolini: Categories and effective computations, in: Lecture Notes in Computer Science 283, Springer, 1987.

    Google Scholar 

  19. D. T. Sannella, A. Tarlecki: Extended ML, an institution-independent framework for formal program development, in: Proc. of Category Theory and Computer Programming (Guildford), Springer LNCS 240, 1987.

    Google Scholar 

  20. R. D. Tennent, Semantics of Programming Languages, Prentice-Hall, 1991.

    Google Scholar 

  21. M. Tofte: Operational Semantics and Polymorphic Type Inference, dissertation, 1988; available as CST-52-88/ECS-LFCS-88-54, Department of Computer Science, University of Edinburgh.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for the Foundations of Computer Science, James Clerk Maxwell Building, The King's Buildings, EH9 3JZ, Edinburgh, Scotland

    Wesley Phoa & Michael Fourman

Authors
  1. Wesley Phoa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Fourman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

W. Kuich

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Phoa, W., Fourman, M. (1992). A proposed categorical semantics for Pure ML. In: Kuich, W. (eds) Automata, Languages and Programming. ICALP 1992. Lecture Notes in Computer Science, vol 623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55719-9_102

Download citation

  • DOI: https://doi.org/10.1007/3-540-55719-9_102

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55719-7

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation