Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Day, B.J.: On closed categories of functors. Lecture Notes in Mathematics, vol. 137, pp. 1–38. Springer, Berlin (1970)
Day, B.J.: An embedding theorem for closed categories. Lecture Notes in Mathematics, vol. 420, pp. 55–65. Springer, Berlin (1973)
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)
Girard, J.-Y.: Interprétation fonctionelle et élimination des coupures dans l’arithm étique d’ordre supérieur. PhD thesis, Université Paris VII (1972)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax and variable binding. Formal Aspects of Computing 13, 341–363 (2002)
Hyland, J.M.E.: A small complete category. Annals of Pure and Applied Logic 40, 135–165 (1988)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, Amsterdam (1999)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10, 470–502 (1988)
O’Hearn, P.: On bunched typing. J. Functional Programming 13, 747–796 (2003)
O’Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
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)
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 http://www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408–425. Springer, Heidelberg (1974)
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)
Seely, R.A.G.: Categorical semantics for higher order polymorphic lambda calculus. Journal of Symbolic Logic 52, 969–989 (1987)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
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)
Walker, D., Watkins, K.: On regions and linear type. In: Proc. International Conference on Functional Programming, pp. 181–192 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collinson, M., Pym, D., Robinson, E. (2005). On Bunched Polymorphism. In: Ong, L. (eds) Computer Science Logic. CSL 2005. Lecture Notes in Computer Science, vol 3634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11538363_5
Download citation
DOI: https://doi.org/10.1007/11538363_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28231-0
Online ISBN: 978-3-540-31897-2
eBook Packages: Computer ScienceComputer Science (R0)