Behavioural specifications in type theory

  • Nikos Mylonakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


In this paper we give a new view of the type theory UTT (Uniform theory of dependent types) [5] as a system to formally develop programs from algebraic specifications, comparable to e.g. EML([9]). We will focus our attention on behavioural specifications since they have not been deeply studied in a type theoretical setting, and we describe how to develop proofs about behavioural satisfaction.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Kent Petersson Bengt Nordström and Jan Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, 1990.Google Scholar
  2. 2.
    M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, and D. Sannella (eds.). Algebraic System Specification and Development: A survey and Annotated Bibliography, volume 501 of LNCS. Springer Verlag, 1991.Google Scholar
  3. 3.
    Michel Bidoit and Rolf Hennicker. Behavioural theories and the proof of behavioural properties. Report LIENS-95-5, Ecole Normale Supérieure, 1995.Google Scholar
  4. 4.
    Michel Bidoit, Rolf Hennicker, and Martin Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25(2–3):149–186, December 1995.Google Scholar
  5. 5.
    Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, September 1994. Also published as Technical Report CST-110-94, Department of Computer Science.Google Scholar
  6. 6.
    Rolf Hennicker. Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 4:326–345, 1991.Google Scholar
  7. 7.
    Martin Hofmann and Donald Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Report ECS-LFCS-95-318, Univ. of Edinburgh, 1995. To appear in Theoretical Computer Science.Google Scholar
  8. 8.
    Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The definition of Extended ML: A gentle introduction. To appear in Theoretical Computer Science.Google Scholar
  9. 9.
    Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The Definition of Extended ML. Technical Report ECS-LFCS-94-300, LFCS, August 1994.Google Scholar
  10. 10.
    Zhaohui Luo. Program specification and data refinement in type theory. Math. Struct. in Comp. Science, 3:333–63, 1993.Google Scholar
  11. 11.
    Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Clarendon Press Oxford, 1994.Google Scholar
  12. 12.
    Zhaohui Luo and Randy Pollack. LEGO proof development system: User's manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, May 1992.Google Scholar
  13. 13.
    Grant Malcolm and Joseph A. Goguen. Proving correctness of refinement and implementation. Technical Monograph PRG-114, Oxford University Computing Laboratory, 1994 (revised May 1995).Google Scholar
  14. 14.
    James Hugh McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, University of Edinburgh, November 1992.Google Scholar
  15. 15.
    Robin Milner and Mads Tofte. Commentary on Standard ML. The MIT Press, 1991.Google Scholar
  16. 16.
    Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990.Google Scholar
  17. 17.
    Simon Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.Google Scholar
  18. 18.
    Judith Underwood. Typing abstract data types. In Springer Verlag, editor, Selected Papers from the 10th Workshop on Specification of Abstract Data Types, Santa Margherita Ligure, number 906 in LNCS, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Nikos Mylonakis
    • 1
  1. 1.Department of Computer ScienceUniversity of EdinburghGermany

Personalised recommendations