Extended ML: Past, present and future | SpringerLink
Skip to main content
Springer Nature Link
Log in

Extended ML: Past, present and future

  • Conference paper
  • First Online:
Recent Trends in Data Type Specification (ADT 1990)

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

Included in the following conference series:

Abstract

An overview of past, present and future work on the Extended ML formal program development framework is given, with emphasis on two topics of current active research: the semantics of the Extended ML specification language, and tools to support formal program development.

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

6 References

  1. A. Appel and D. MacQueen. A Standard ML compiler. Proc. Conf. on Functional Programming and Computer Architecture, Portland. LNCS 274 Springer Lecture Notes in Computer Science, Volume 274 (1987).

    Google Scholar 

  2. J. Bergstra, J. Heering and P. Klint. Module algebra. Journal of the Assoc. for Computing Machinery 37(2), 335–372 (1990).

    Google Scholar 

  3. M. Bidoit. PLUSS, un langage pour le développement de spécifications algébriques modulaires. Thèse d'Etat, Université Paris-Sud, Orsay (1989).

    Google Scholar 

  4. R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall (1988).

    Google Scholar 

  5. R. Boyer and J. Moore. A Computational Logic Handbook. Academic Press (1988).

    Google Scholar 

  6. M. Broy and M. Wirsing. Partial abstract data types. Acta Informatica 18(1), 47–64 (1982).

    Article  Google Scholar 

  7. R. Burstall. Computer-assisted proof for mathematics: an introduction, using the Lego proof system. Proc. IAM Conf. on The Revolution in Mathematics Caused by Computing, Brighton (1989).

    Google Scholar 

  8. R. Burstall, D. MacQueen and D. Sannella. HOPE: an experimental applicative language. Proc. 1980 LISP Conference, Stanford, 136–143 (1980).

    Google Scholar 

  9. T. Coquand. An analysis of Girard's paradox. Proc. IEEE Symp. on Logic in Computer Science, Cambridge (1986).

    Google Scholar 

  10. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science, Vol. 6. Springer (1985).

    Google Scholar 

  11. J. Farrés-Casals. Proving correctness of constructor implementations. Proc. 1989 Symp. on Mathematical Foundations of Computer Science. LNCS 379, 225–235 (1989).

    Google Scholar 

  12. J. Farrés-Casals. Proving correctness w.r.t. specifications with hidden parts. Proc. 2nd Intl. Conf. on Algebraic and Logic Programming, Nancy. LNCS 463, 25–39 (1990).

    Google Scholar 

  13. J. Farrés-Casals. Verification in ASL and Related Specification Languages. Ph.D. thesis, Univ. of Edinburgh, to appear (1991).

    Google Scholar 

  14. L. Feijs, H. Jonkers, C. Koymans and G. Renardel de Lavalette. Formal definition of the design language COLD-K. METEOR Report t7/PRLE/7, Philips Research Lab., Eindhoven (1987).

    Google Scholar 

  15. J. Goguen and R. Burstall. Introducing institutions. Proc. Logics of Programming Workshop, Carnegie-Mellon. LNCS 164, 221–256 (1984).

    Google Scholar 

  16. J. Goguen and T. Winkler. Introducing OBJ3. Research report, SRI International (1988).

    Google Scholar 

  17. M. Gordon, R. Milner and C. Wadsworth. Edinburgh LCF. LNCS 78 Springer Lecture Notes in Computer Science, Volume 78 (1979).

    Google Scholar 

  18. M. Gordon and A. Pitts. The HOL logic. Part II of The HOL System: Description. DSTO Australia and SRI International (preliminary version), November 1989.

    Google Scholar 

  19. R. Harper. Introduction to Standard ML. Report ECS-LFCS-86-14, Univ. of Edinburgh. Revised edition (1989).

    Google Scholar 

  20. R. Harper, J. Mitchell and E. Moggi. Higher-order modules and the phase distinction. Proc. 17th ACM Symp. on Principles of Programming Languages (1990).

    Google Scholar 

  21. I. Hayes and C. Jones. Specifications are (not necessarily) executable. Software Engineering Journal 4(6), 320–338 (1989).

    Google Scholar 

  22. R. Hennicker. Context induction: a proof principle for behavioural abstractions. Proc. Intl. Symp. on Design and Implementation of Symbolic Computation Systems, Capri. LNCS 429, 101–110 (1990).

    Google Scholar 

  23. J. Hook and R. Kieburtz. Key Words in Context: an example. Technical Report CSE-90-012, Oregon Graduate Institute (1990).

    Google Scholar 

  24. P. Hudak and P. Wadler et al. Report on the functional programming language Haskell. Report CSC/89/R5, Univ. of Glasgow (1989).

    Google Scholar 

  25. H. Hußmann. Rapid prototyping for algebraic specifications: RAP system user's manual. Report MIP-8504, Universität Passau (1985).

    Google Scholar 

  26. C. Jones. Systematic Software Development Using VDM. Prentice-Hall (1986).

    Google Scholar 

  27. B. Krieg-Brückner and D. Sannella. Structuring specifications in-the-large and in-the-small: higher-order functions, dependent types and inheritance in SPECTRAL. Proc. Joint Conf. on Theory and Practice of Software Development, Brighton, April 1991. LNCS, to appear (1991).

    Google Scholar 

  28. Z. Luo, R. Pollack and P. Taylor. How to use Lego (a preliminary user's manual). Report LFCS-TN-27, Univ. of Edinburgh (1989).

    Google Scholar 

  29. D. MacQueen. Modules for Standard ML. In: Report ECS-LFCS-86-2, Univ. of Edinburgh (1986).

    Google Scholar 

  30. D. MacQueen. Using dependent types to express modular structure: experience with Pebble and ML. Proc. 13th ACM Symp. on Principles of Programming Languages (1986).

    Google Scholar 

  31. D. MacQueen and D. Sannella. Completeness of proof systems for equational specifications. IEEE Transactions on Software Engineering SE-11, 454–461 (1985).

    Google Scholar 

  32. C. Meldrum and A.W. Smith. Design of an SML to Ten15 compiler. Harlequin Ltd. (1990).

    Google Scholar 

  33. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348–375 (1978).

    Article  Google Scholar 

  34. R. Milner. Communication and Concurrency. Prentice-Hall (1989).

    Google Scholar 

  35. R. Milner and M. Tofte. Commentary on Standard ML. MIT Press (1990).

    Google Scholar 

  36. R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. MIT Press (1990).

    Google Scholar 

  37. J. Mitchell. Representation independence and data abstraction. Proc. 13th ACM Symp. on Principles of Programming Languages (1986).

    Google Scholar 

  38. J. Mitchell and R. Harper. The essence of ML. Proc. 15th ACM Symp. on Principles of Programming Languages (1988).

    Google Scholar 

  39. L. Paulson. Natural deduction proof as higher-order resolution. Journal of Logic Programming 3, 237–258 (1986).

    Google Scholar 

  40. L. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Univ. Press (1987).

    Google Scholar 

  41. L. Paulson and T. Nipkow. Isabelle tutorial and user's manual. Report 189, Cambridge University (1990).

    Google Scholar 

  42. G. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University (1981).

    Google Scholar 

  43. C. Reade. Elements of Functional Programming. Addison-Wesley (1989).

    Google Scholar 

  44. H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford Univ. Press (1987).

    Google Scholar 

  45. D. Sannella. Semantics, Implementation and Pragmatics of CLEAR, a Program Specification Language. Ph.D. thesis CST-17-82, Univ. of Edinburgh (1982).

    Google Scholar 

  46. D. Sannella. Formal specification of ML programs. Jornadas Rank Xerox Sobre Inteligencia Artificial Razonamiento Automatizado, Blanes, Spain, 79–98 (1987).

    Google Scholar 

  47. D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park, January 1990. LNCS, to appear (1991).

    Google Scholar 

  48. D. Sannella and R. Burstall. Structured theories in LCF. Proc. 8th Colloq. on Trees in Algebra and Programming, L'Aquila, Italy. LNCS 159, 377–391 (1983).

    Google Scholar 

  49. D. Sannella, F. da Silva and A. Tarlecki. Syntax, typechecking and dynamic semantics for Extended ML (version 2). Draft report, Univ. of Edinburgh (1990). Version 1 appeared as Report ECS-LFCS-89-101, Univ. of Edinburgh (1989).

    Google Scholar 

  50. D. Sannella, S. Sokolowski and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Report 6/90, Univ. of Bremen (1990).

    Google Scholar 

  51. D. Sannella and A. Tarlecki. Program specification and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, 67–77 (1985).

    Google Scholar 

  52. D. Sannella and A. Tarlecki. Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming, Guildford. LNCS 240, 364–389 (1986).

    Google Scholar 

  53. D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34, 150–178 (1987).

    Google Scholar 

  54. D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988).

    Article  Google Scholar 

  55. D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25, 233–281 (1988).

    Google Scholar 

  56. D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Proc. Joint Conf. on Theory and Practice of Software Development, Barcelona. LNCS 352, 375–389 (1989). Full version as Report ECS-LFCS-89-71, Univ. of Edinburgh (1989).

    Google Scholar 

  57. D. Sannella and A. Tarlecki. A kernel specification formalism with higher-order parameterisation. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, GDR; LNCS, this volume (1991).

    Google Scholar 

  58. D. Sannella and L. Wallen. A calculus for the construction of modular Prolog programs. Proc. 1987 IEEE Symp. on Logic Programming, San Francisco, 368–378 (1987); to appear in Journal of Logic Programming.

    Google Scholar 

  59. D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. LNCS 158, 413–427 (1983).

    Google Scholar 

  60. W. Scherlis and D. Scott. First steps towards inferential programming. Information Processing '83, 199–212. North-Holland (1983).

    Google Scholar 

  61. O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis CST-42-87, Univ. of Edinburgh (1987).

    Google Scholar 

  62. A. Stevens. An Improved Method for the Mechanisation of Inductive Proof. Ph.D. thesis, Univ. of Edinburgh (1990).

    Google Scholar 

  63. T. Stroup, N. Gőtz and M. Mendler. Stepwise refinement of layered protocols by formal program development. Proc. 9th Conf. on Protocol Specification, Testing, and Verification, North-Holland (1989).

    Google Scholar 

  64. M. Tofte. Operational Semantics and Polymorphic Type Inference. Ph.D. thesis CST-52-88, Univ. of Edinburgh (1988).

    Google Scholar 

  65. M. Tofte. Four lectures on Standard ML. Report ECS-LFCS-89-73, Univ. of Edinburgh (1989).

    Google Scholar 

  66. Å. Wikström. Functional Programming Using Standard ML. Prentice-Hall (1987).

    Google Scholar 

  67. M. Wirsing. Structured algebraic specifications: a kernel language. Theoretical Computer Science 42, 123–249 (1986).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, Scotland

    Donald Sannella

  2. Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

    Andrzej Tarlecki

Authors
  1. Donald Sannella
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Tarlecki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

H. Ehrig K. P. Jantke F. Orejas H. Reichel

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sannella, D., Tarlecki, A. (1991). Extended ML: Past, present and future. In: Ehrig, H., Jantke, K.P., Orejas, F., Reichel, H. (eds) Recent Trends in Data Type Specification. ADT 1990. Lecture Notes in Computer Science, vol 534. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54496-8_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-54496-8_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54496-8

  • Online ISBN: 978-3-540-38416-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation