Type Checking Parametrised Programs and Specifications in ASL + FPC

  • David Aspinall
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


ASL+ [SST92] is a kernel specification language with higher-order parametrisation for programs and specifications, based on a dependently typed λ-calculus. ASL+ has an institution-independent semantics, which leaves the underlying programming language and specification logic unspecified. To complete the definition, and in particular, to study the type checking problem for ASL+, the language ASL+FPC was conceived. It is a modified version of ASL+ for \(\mathcal{FPC}\), and institution based on the paradigmatic programming calculus FPC. The institution \(\mathcal{FPC}\) is notable for including sharing equations inside signatures, reminiscent of so-called manifest types or translucent sums in type systems for programming language modules [Ler94,HL94]. This allows type equalities to be propagated when composing modules. This paper introduces \(\mathcal{FPC}\) and ASL+FPC and their type checking systems.


Program Language Parametrise Program Type Check Typing Judgement Signature Morphism 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Asp95a]
    Aspinall, D.: Subtyping with singleton types. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, Springer, Heidelberg (1995)CrossRefGoogle Scholar
  2. [Asp95b]
    Aspinall, D.: Types, subtypes, and ASL+. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  3. [Asp97]
    Aspinall, D.: Type Systems for Modular Programs and Specification. PhD thesis, Department of Computer Science, University of Edinburgh (1997)Google Scholar
  4. [Cen94]
    Cengarle, M.V.: Formal Specifications with Higher-Order Parameterisation. PhD thesis, Institut für Informatik, Ludwig-Maximilians- Universität München (1994)Google Scholar
  5. [DCH03]
    Dreyer, D., Crary, K., Harper, R.: A type system for higherorder modules. In: Proceedings of POPL 2003, New Orleans (2003)Google Scholar
  6. [GB92]
    Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39, 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  7. [GM93]
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  8. [Gun92]
    Gunter, C.A.: Semantics of Programming Languages. MIT Press, Cambridge (1992)zbMATHGoogle Scholar
  9. [HL94]
    Harper, R., Lillibridge, M.: A type-theoretic approach to higherorder modules with sharing. In: Conference Record of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994), Portland, Oregon, January 17–21, pp. 123–137. ACM Press, New York (1994)CrossRefGoogle Scholar
  10. [HMM90]
    Harper, R., Mitchell, J.C., Moggi, E.: Higher-order modules and the phase distinction. In: Conference record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, CA, January 1990, pp. 341–354 (1990)Google Scholar
  11. [Jon96]
    Jones, M.P.: Using parameterized signatures to express modular structure. In: Conference Record of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1996), St. Petersburg, Florida, pp. 21–24. ACM Press, New York (1996)Google Scholar
  12. [Jud97]
    Courant, J.: An applicative module calculus. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 622–636. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. [Ler94]
    Leroy, X.: Manifest types, modules, and separate compilation. In: Proc. 21st symp. Principles of Programming Languages, pp. 109–122. ACM press, New York (1994)Google Scholar
  14. [Ler95]
    Leroy, X.: Applicative functors and fully transparent higher-order modules. In: Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995), San Francisco, California, January 22–25, pp. 142–153. ACM Press, New York (1995)CrossRefGoogle Scholar
  15. [Ler96]
    Leroy, X.: A syntactic theory of type generativity and sharing. Journal of Functional Programming 6(5), 667–698 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  16. [Mac86]
    MacQueen, D.: Using dependent types to express modular structure. In: Proceedings, Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 13–15. ACM SIGACT-SIGPLAN, pp. 277–286. ACM Press, New York (1986)Google Scholar
  17. [MNOS99]
    Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9, 191–223 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  18. [Mos99]
    Mossakowski, T.: Specifications in an arbitrary institution with symbols. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 252–270. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. [Plo85]
    Plotkin, G.: Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School (1985)Google Scholar
  20. [Rus99]
    Russo, C.V.: Non-dependent types for standard ML modules. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 80–97. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. [SH00]
    Stone, C.A., Harper, R.: Deciding type equivalence in a language with singleton kinds. In: ACM Symposium on Principles of Programming Languages (POPL), Boston, Massachusetts, pp. 214–227, January 19–21 (2000)Google Scholar
  22. [Sha98]
    Shao, Z.: Parameterized signatures and higher-order modules, 1998. Technical Report YALEU/DCS/TR-1161, Dept. of Computer Science, Yale University (August 1998)Google Scholar
  23. [Sha99]
    Shao, Z.: Transparent modules with fully syntactic signatures. In: International Conference on Functional Programming, pp. 220–232 (1999)Google Scholar
  24. [SM02]
    Schröder, L., Mossakowski, T.: HasCASL: Towards integrated specification and development of Haskell programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 99. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. [SMT+01]
    Schröder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Semantics of Architectural Specifications in CASL. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 253–268. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. [SST92]
    Sannella, D., Sokołowski, S., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica 29, 689–736 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  27. [ST86]
    Sannella, D., Tarlecki, A.: Extended ML: An institutionindependent framework for formal program development. In: Poigné, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 364–389. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  28. [ST88]
    Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica 25, 233–281 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  29. [Tar92]
    Tarlecki, A.: Modules for a model-oriented specification language: a proposal for MetaSoft. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 452–472. Springer, Heidelberg (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • David Aspinall
    • 1
  1. 1.School of InformaticsUniversity of EdinburghUK

Personalised recommendations