On Bunched Polymorphism

Extended Abstract
  • Matthew Collinson
  • David Pym
  • Edmund Robinson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We describe a polymorphic extension of the substructural lambda calculus αλ associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers are presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.


Equivalence Class Type System Type Variable Semantic Type Linear Logic 
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. 1.
    Day, B.J.: On closed categories of functors. Lecture Notes in Mathematics, vol. 137, pp. 1–38. Springer, Berlin (1970)Google Scholar
  2. 2.
    Day, B.J.: An embedding theorem for closed categories. Lecture Notes in Mathematics, vol. 420, pp. 55–65. Springer, Berlin (1973)Google Scholar
  3. 3.
    Girard, J.-Y.: Une extension de l’interprétation de Gödel à l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Proc. 2nd Scandinavian Logic Symposium, pp. 63–92. North-Holland, Amsterdam (1971)CrossRefGoogle Scholar
  4. 4.
    Girard, J.-Y.: Interprétation fonctionelle et élimination des coupures dans l’arithm étique d’ordre supérieur. PhD thesis, Université Paris VII (1972)Google Scholar
  5. 5.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax and variable binding. Formal Aspects of Computing 13, 341–363 (2002)zbMATHCrossRefGoogle Scholar
  7. 7.
    Hyland, J.M.E.: A small complete category. Annals of Pure and Applied Logic 40, 135–165 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, Amsterdam (1999)zbMATHGoogle Scholar
  9. 9.
    Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10, 470–502 (1988)CrossRefGoogle Scholar
  10. 10.
    O’Hearn, P.: On bunched typing. J. Functional Programming 13, 747–796 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    O’Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Prawitz, D.: Proofs and the meaning and completeness of logical constants. In: Essays on mathematical and philosophical logic, pp. 25–40. D. Reidel, Dordrecht (1978)Google Scholar
  13. 13.
    Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers, Dordrecht (2002), Errata at zbMATHGoogle Scholar
  14. 14.
    Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408–425. Springer, Heidelberg (1974)Google Scholar
  15. 15.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structure. In: Proc. LICS 2002, pp. 55–74. IEEE Computer Science Press, Los Alamitos (2002)Google Scholar
  16. 16.
    Seely, R.A.G.: Categorical semantics for higher order polymorphic lambda calculus. Journal of Symbolic Logic 52, 969–989 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Walker, D., Morrisett, J.G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 177–206. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Walker, D., Watkins, K.: On regions and linear type. In: Proc. International Conference on Functional Programming, pp. 181–192 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Matthew Collinson
    • 1
  • David Pym
    • 1
  • Edmund Robinson
    • 2
  1. 1.University of BathUK
  2. 2.Queen Mary, University of LondonUK

Personalised recommendations