Advertisement

Deliverables: a categorical approach to program development in type theory

  • James McKinna
  • Rod Burstall
Invited Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)

Abstract

We describe a method for formally developing functional programs using the “propositions as types” paradigm. The idea is that a function together with its proof of correctness forms a morphism in a category whose objects are input/output specifications. The functionproof pairs, called “deliverables”, can be combined by the operations of a cartesian closed category, indeed by the same operations which are usually used to combine functions. The method has been implemented using the Lego proof assistant and tried on some examples.

Keywords

Type Theory Function Component Correctness Proof True Predicate Elimination Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J.Bénabou, Fibred categories and the foundations of naïve category theory, JSL, 1985.Google Scholar
  2. 2.
    S. Berardi, Type Dependence and Constructive Mathematics, Ph.D. thesis, Dipartimento di Informatica, Torino, Italy 1990.Google Scholar
  3. 3.
    N.G. de Bruijn, A survey of the project AUTOMATH, in: [35].Google Scholar
  4. 4.
    R.M.Burstall and J.H.McKinna, Deliverables: an approach to program development in Constructions, in [15], also available as a University of Edinburgh technical report ECS-LFCS-91-133.Google Scholar
  5. 5.
    R.Constable et al., Implementing Mathematics with the NuPrl Proof Development System, Prentice-Hall, New Jersey, 1986.Google Scholar
  6. 6.
    T.Coquand and G.Huet, Constructions: a Higher-order Proof system for mechanizing mathematics, in: Proceedings EUROCAL '85, LNCS 203, Springer-Verlag, 1985.Google Scholar
  7. 7.
    T.Coquand, Metamathematical Investigations of a Calculus of Constructions, in: [14].Google Scholar
  8. 8.
    P-L.Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman Research Notes in Theoretical Computer Science, Pitman, London, 1986.Google Scholar
  9. 9.
    J-Y.Girard, Interpretation fonctionelle et élimination des coupures dans l'arithmétique de l'ordre supérieure, thesis, University of Paris VII, 1972.Google Scholar
  10. 10.
    S.Hayashi, Adjunction of semifunctors: categorical structures in nonextensional lambda calculus, in Theoretical Computer Science, Vol. 41, North-Holland, Amsterdam, 1985.Google Scholar
  11. 11.
    S.Hayashi, Singleton, Union and Intersection Types for Program Extraction, in: Proceedings of TACS '91, Sendai, Japan, Springer LNCS 526, Springer-Verlag, 1991.Google Scholar
  12. 12.
    C.A.R.Hoare, An axiomatic basis for computer programming, in: Communications of the ACM, Vol. 12, 1969.Google Scholar
  13. 13.
    W.A.Howard, The “formulae-as-types” notion of construction, in: [35].Google Scholar
  14. 14.
    G.Huet, T.Coquand, C.Paulin-Mohring et al., The Calculus of Constructions, Version 4-10, Documentation and user's manual, Rapports Techniques no.110, Projet Formel, INRIA-Rocquencourt, Paris, August 1989.Google Scholar
  15. 15.
    G.Huet and G.Plotkin, eds. Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks, Antibes, May 1990, distributed electronically to participating BRA sites, January 1991.Google Scholar
  16. 16.
    J.M.E.Hyland and A.M.Pitts, The Theory of Constructions: Categorical Semantics and Topos-theoretic models, in: Proceedings of the AMS Conference on Categories in Computer Science, Boulder, Colorado, 1986.Google Scholar
  17. 17.
    P.T.Johnstone and R.Paré, eds., Indexed Categories and their Applications, Springer LNM 661, Springer-Verlag, 1978.Google Scholar
  18. 18.
    J.Lambek and P.J.Scott, An Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics no. 7, Cambridge University Press, Cambridge, England, 1986.Google Scholar
  19. 19.
    Z.Luo, ECC, an Extended Calculus of Constructions, in: Proceedings of the Fourth IEEE Conference on Logic in Computer Science, Asilomar, California, 1989.Google Scholar
  20. 20.
    Z.Luo, An Extended Calculus of Constructions, Ph.D. Thesis, Department of Computer Science, University of Edinburgh, June 1990.Google Scholar
  21. 21.
    Z.Luo, Program Specification and Data Refinement in Type Theory, Technical Report ECS-LFCS-90-131, Department of Computer Science, University of Edinburgh, January 1991.Google Scholar
  22. 22.
    Z.Luo and R.Pollack, LEGO Proof Development System: User's Manual, LFCS Technical Report ECS-LFCS-92-211, 1992.Google Scholar
  23. 23.
    J.H.McKinna, Deliverables: a categorical approach to program development in type theory, Ph.D. thesis, University of Edinburgh, 1992.Google Scholar
  24. 24.
    P.Martin-Löf, An Intuitionistic Theory of Types: Predicative part, in: Logic Colloquium 73, North-Holland, Amsterdam, 1975.Google Scholar
  25. 25.
    P.Martin-Löf, Constructive Mathematics and Computer Programming, in: proceedings of the Conference on Logic, Philosophy and Methodology of Science VI, 1979, North-Holland, Amsterdam, 1982.Google Scholar
  26. 26.
    M.Mendler, The Logic of Design, Ph.D. thesis, University of Edinburgh, forthcoming, 1992.Google Scholar
  27. 27.
    B.Nordström, K.Petersson, and J.Smith, Programming in Martin-Löf's type theory, Oxford University Press, 1990.Google Scholar
  28. 28.
    C.Paulin-Mohring, Extracting F ω 's programs from proofs in the Calculus of Constructions, in: Proceedings POPL89, ACM, 1989.Google Scholar
  29. 29.
    C.Paulin-Mohring and B.Werner, Extracting and Executing Programs developed in the Inductive Constructions System: a Progress Report, in: [15].Google Scholar
  30. 30.
    D.Pavlovič, Predicates and Fibrations, proefschrift, University of Utrecht, 1990.Google Scholar
  31. 31.
    R.A.Pollack, Implicit Syntax, in: [15].Google Scholar
  32. 32.
    A.Salvesen and J.Smith, On the strength of the subset type in Martin-Löfs type theory, in: Proceedings of the Third LICS Symposium, IEEE, 1988.Google Scholar
  33. 33.
    A.Salvesen, On Information Discharging and Retrieval in Martin-Löf's type theory, Ph.D. thesis, Institute of Informatics, University of Oslo, 1989.Google Scholar
  34. 34.
    D.Sannella, Formal specification of ML programs, LFCS technical report ECS-LFCS-86-15, Dept. of Computer Science, University of Edinburgh, 1986.Google Scholar
  35. 35.
    J.P.Seldin and J.R.Hindley, eds., To H.B.Curry, essays in Combinatory Logic, λ-calculus and Formalism, Academic Press, 1980.Google Scholar
  36. 36.
    B.Reus and T.Streicher, Verifying Properties of Module Constructions in Type Theory, this volume.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • James McKinna
    • 1
  • Rod Burstall
    • 1
    • 2
  1. 1.Laboratory for the Foundations of Computer ScienceUniversity of EdinburghUK
  2. 2.J.C.M.B.EdinburghUK

Personalised recommendations