Relational parametricity for references and recursive types

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Relational parametricity for references and recursive types

Full text

Pdf (588 KB)

Source

Types In Languages Design And Implementation archive
Proceedings of the 4th international workshop on Types in language design and implementation table of contents

Savannah, GA, USA

SESSION: Session 3 table of contents

Pages 91-104

Year of Publication: 2009

ISBN:978-1-60558-420-1

Authors

Lars Birkedal	IT University of Copenhagen, DK-2300 Copenhagen S, Denmark
Kristian Støvring	IT University of Copenhagen, DK-2300 Copenhagen S, Denmark
Jacob Thamsborg	IT University of Copenhagen, DK-2300 Copenhagen S, Denmark

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 37, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1481861.1481873 What is a DOI?

ABSTRACT

We present a possible world semantics for a call-by-value higher-order programming language with impredicative polymorphism, general references, and recursive types. The model is one of the first relationally parametric models of a programming language with all these features.

To model impredicative polymorphism we define the semantics of types via parameterized (world-indexed) logical relations over a universal domain. It is well-known that it is non-trivial to show the existence of logical relations in the presence of recursive types. Here the problems are exacerbated because of general references. We explain what the problems are and present our solution, which makes use of a novel approach to modeling references. We prove that the resulting semantics is adequate with respect to a standard operational semantics and include simple examples of reasoning about contextual equivalence via parametricity.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	M. Abadi and G. Plotkin. A per model of polymorphism and recursive types. In Proceedings of LICS, pages 355--365, 1990.
	2	A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proc. of ESOP, pages 69--83, 2006.
	3	Amal Ahmed , Derek Dreyer , Andreas Rossberg, State-dependent representation independence, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	4	Roberto M. Amadio, Recursion over realizability structures, Information and Computation, v.91 n.1, p.55-85, March 1991 [doi>10.1016/0890-5401(91)90074-C]
	5	Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
	6	Andrew W. Appel , Paul-André Melliès , Christopher D. Richards , Jérôme Vouillon, A very modal model of a modern, major, general type system, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
	7	N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In Proc. of TLCA, volume 3461 of LNCS, 2005.
	8	G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Proc. of HOOTS, volume 41 of ENTCS, 2000.
	9	Lars Birkedal , Rasmus E. Møgelberg, Categorical models for Abadi and Plotkin's logic for parametricity, Mathematical Structures in Computer Science, v.15 n.4, p.709-772, August 2005 [doi>10.1017/S0960129505004834]
	10	L. Birkedal, R. E. Møgelberg, and R. L. Petersen. Linear Abadi & Plotkin logic. Logical Methods in Computer Science, 2(5:1):1--33, 2006.
	11	N. Bohr and L. Birkedal. Relational reasoning for recursive types and references. In Proc. of APLAS, pages 79--96, 2006.
	12	N. Bohr and L. Birkedal. Relational parametricity for recursive types and references of closed types. Technical report, IT University of Copenhagen, 2007. A Chapter in Nina Bohr's Ph.D. dissertation 2007.
	13	Karl Crary , Robert Harper, Syntactic Logical Relations for Polymorphic and Recursive Types, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.259-299, April, 2007 [doi>10.1016/j.entcs.2007.02.010]
	14	Andrzej Filinski, On the relations between monadic semantics, Theoretical Computer Science, v.375 n.1-3, p.41-75, April, 2007 [doi>10.1016/j.tcs.2006.12.027]
	15	M. Hasegawa. Relational parametricity and control. Logical Methods in Computer Science, 2(3):1--22, 2006.
	16	Patricia Johann, On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi, Mathematical Structures in Computer Science, v.15 n.2, p.201-229, April 2005 [doi>10.1017/S0960129504004578]
	17	Patricia Johann , Janis Voigtländer, The Impact of seq on Free Theorems-Based Program Transformations, Fundamenta Informaticae, v.69 n.1-2, p.63-102, July 2005
	18	V. Koutavas and M. Wand. Bisimulations for untyped imperative objects. In Proc. of ESOP, pages 146--161, 2006.
	19	Vasileios Koutavas , Mitchell Wand, Small bisimulations for reasoning about higher-order imperative programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.141-152, January 11-13, 2006, Charleston, South Carolina, USA
	20	Soren B. Lassen , Paul Blain Levy, Typed Normal Form Bisimulation for Parametric Polymorphism, Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, p.341-352, June 24-27, 2008 [doi>10.1109/LICS.2008.26]
	21	S. B. Lassen and P. B. Levy. Typed normal form bisimulation. In Proc. of CSL, volume 4646 of LNCS, pages 283--297, 2007.
	22	Paul Blain Levy, Possible World Semantics for General Storage in Call-By-Value, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.232-246, September 22-25, 2002
	23	Paul-Andre Mellies , Jerome Vouillon, Recursive Polymorphic Types and Parametricity in an Operational Framework, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.82-91, June 26-29, 2005 [doi>10.1109/LICS.2005.42]
	24	R. Møgelberg. Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism. In Proc. of ICALP, pages 372--383, 2006.
	25	Rasmus Ejlers Mogelberg , Alex Simpson, Relational Parametricity for Computational Effects, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.346-355, July 10-14, 2007 [doi>10.1109/LICS.2007.40]
	26	Rasmus Ejlers Møgelberg , Alex Simpson, Relational Parametricity for Control Considered as a Computational Effect, Electronic Notes in Theoretical Computer Science (ENTCS), 173, p.295-312, April, 2007 [doi>10.1016/j.entcs.2007.02.040]
	27	Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
	28	A. M. Pitts. Relational properties of domains. Information and Computation, 127:66--90, 1996.
	29	Andrew M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, v.10 n.3, p.321-359, June 2000 [doi>10.1017/S0960129500003066]
	30	A. M. Pitts. Advanced Topics in Types and Programming Languages, chapter Typed Operational Reasoning. The MIT Press, 2005.
	31	Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
	32	G. Plotkin. Second order type theory and recursion. Notes for a talk at the Scott Fest, Feb. 1993.
	33	Gordon D. Plotkin , Martín Abadi, A Logic for Parametric Polymorphism, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.361-375, March 16-18, 1993
	34	J. Reynolds. Types, abstraction, and parametric polymorphism. Information Processing, 83:513--523, 1983.
	35	Kristian Støvring , Soren B. Lassen, A complete, co-inductive syntactic theory of sequential control and state, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
	36	Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.63-74, January 12-14, 2005, Long Beach, California, USA
	37	Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]