L^3 : A Linear Language with Locations

• Autorzy: Ahmed A. , Fluet M. , Morrisett G.
• Języki publikacji: EN

Abstrakty

EN

We present a simple, but expressive type system that supports strong updates-updating a memory cell to hold values of unrelated types at different points in time. Our formulation is based upon a standard linear lambda calculus and, as a result, enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact that our core programming language supports shared, mutable references and cyclic graphs, every well-typed program terminates. We then consider extensions needed to model ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for re-gaining the capability to perform strong updates on unrestricted references. The thaw primitive is closely related to other mechanisms that support strong updates, such as CQUAL's restrict.

Słowa kluczowe

EN

linearity and strong update

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 397--449
• Opis fizyczny: bibliogr. 46 poz.

Twórcy

autor

Ahmed A.

autor

Fluet M.

autor

Morrisett G.

• Toyota Technological Institute at Chicago, Chicago, 1427 East 60th St, Chicago, IL 60637, USA,

Bibliografia

• [1] Abramsky, S.: Computational interpretations of linear logic, Theoretical Computer Science, 111(1-2), 1993, 3-57.
• [2] Achten, P., Plasmeijer, R.: The ins and outs of Clean I/O, Journal of Functional Programming, 5(1), 1995, 81-110.
• [3] Ahmed, A., Appel, A.W., Virga, R.: An IndexedModel of Impredicative Polymorphism and Mutable References, January 2003, Available at http://www.cs.princeton.edu/_appel/papers/impred.pdf.
• [4] Ahmed, A., Fluet, M., Morrisett, G.: L3: A Linear Language with Locations, Technical Report TR-24-04, Harvard University, October 2004.
• [5] Ahmed, A. J.: Semantics of Types for Mutable State, Ph.D. Thesis, Princeton University, 2004.
• [6] Aiken, A., Foster, J. S., Kodumal, J., Terauchi, T.: Checking and Inferring Local Non-Aliasing, Proc. ACM Conference on Programming Language Design and Implementation (PLDI), June 2003.
• [7] Almeida, P. S.: Balloon Types: Controlling sharing of state in data types., European Conference on Object-Oriented Programming (ECOOP), June 1997.
• [8] Appel, A.W., McAllester, D.: An IndexedModel of Recursive Types for Foundational Proof-Carrying Code, ACM Transactions on Programming Languages and Systems, 23(5), September 2001, 657-683.
• [9] Aspinall, D., Compagnoni, A.: Heap Bounded Assembly Language, Journal of Automated Reasoning, 31, 2003, 261-302.
• [10] Aspinall, D., Hofmann, M.: Another Type System for In-Place Update, Proc. European Symposium on Programming (D. L. Metayer, Ed.), Springer-Verlag, 2002, LNCS 2305.
• [11] Baker, H.: Lively Linear LISP-Look Ma, No Garbage, ACM SIGPLAN Notices, 27(8), 1992, 89-98.
• [12] Barber, A.: Dual Intuitionistic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh, September 1996.
• [13] Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A Term Calculus for Intuitionistic Linear Logic, in: Proceedings Intl. Conf. on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, The Netherlands, 16-18 March 1993 (M. Bezem, J. F. Groote, Eds.), vol. 664, Springer-Verlag, Berlin, 1993, 75-90.
• [14] Benton, P. N.: Strong normalisation for the linear term calculus, Journal of Functional Programming, 5(1), January 1995, 65-80.
• [15] Boyapati, C., Sǎlcianu, A., Beebee,W., Rinard, M.: Ownership Types for Safe Region-Based Memory Management in Real-Time Java, Proc. ACM Conference on Programming Language Design and Implementation (PLDI), June 2003.
• [16] Boyland, J.: Alias Burying: Unique Variables Without Destructive Reads, Software - Practice and Experience, 31(6), 2001, 533-553.
• [17] Boyland, J., Noble, J., Retert, W.: Capabilities for aliasing: A generalization of uniqueness and read-only, European Conference on Object-Oriented Programming (ECOOP), 2001.
• [18] Boyland, J. T., Retert, W.: Connecting effects and uniqueness with adoption, Proc. ACM Symposium on Principles of Programming Languages (POPL), January 2005.
• [19] Cheney, J., Morrisett, G.: A Linearly Typed Assembly Language, Technical Report 2003-1900, Department of Computer Science, Cornell University, 2003.
• [20] Clarke, D.: Object Ownership and Containment, Ph.D. Thesis, School of Computer Science and Engineering, University of New South Wales, 2001.
• [21] Clarke, D., Wrigstad, T.: External Uniqueness is Unique Enough, European Conference on Object-Oriented Programming (ECOOP), July 2003.
• [22] Clarke, D. G., Potter, J. M., Noble, J.: Ownership types for flexible alias protection, ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1998.
• [23] DeLine, R., F¨ahndrich,M.: Enforcing High-Level Protocols in Low-Level Software, Proc. ACM Conference on Programming Language Design and Implementation (PLDI), June 2001.
• [24] F¨ahndrich,M., DeLine, R.: Adoption and Focus: Practical Linear Types for Imperative Programming, Proc. ACM Conference on Programming Language Design and Implementation (PLDI), June 2002.
• [25] Girard, J.-Y.: Linear Logic, Theoretical Computer Science, 50, 1987, 1-102.
• [26] Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating objects with confined types, ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2001.
• [27] Hicks, M., Morrisett, G., Grossman, D., Jim, T.: Experience with Safe Manual Memory-Management in Cyclone, Proc. International Symposium on Memory Management, October 2004.
• [28] Hofmann,M.: A type system for bounded space and functional in-place update, Proc. European Symposium on Programming (ESOP), March 2000.
• [29] Hogg, J.: Islands: Aliasing protection in object-oriented languages, ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), November 1991.
• [30] Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus, Proc. ACM Symposium on Principles of Programming Languages (POPL), January 2001.
• [31] Ishtiaq, S., O'Hearn, P.: BI as an assertion language for mutable data structures, 28th ACM Symposium on Principles of Programming Languages (POPL), London, UK, January 2001.
• [32] Kobayashi, N., Pierce, B. C., Turner, D. N.: Linearity and the Pi-Calculus, ACM Transactions on Programming Languages and Systems, 21(5), 1999, 914-947.
• [33] Kuncak, V., Lam, P., Rinard,M.: Role analysis, Proceedings of the 29th ACMSIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press, 2002, ISBN 1-58113-450-9.
• [34] Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F.,Walker, D.,Weirich, S., Zdancewic, S.: TALx86: A Realistic Typed Assembly Language, Workshop on Compiler Support for Systems Software, Atlanta, GA, May 1999, Published as INRIA Technical Report 0288, March, 1999.
• [35] Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-Based Typed Assembly Language, Journal of Functional Programming, 12(1), January 2002, 43-88.
• [36] Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language, ACM Transactions on Programming Languages and Systems, 21(3),May 1999, 528-569.
• [37] O'Hearn, P. W., Reynolds, J. C.: From Algol to polymorphic linear lambda-calculus, Journal of the ACM, 47(1), 2000, 167-223, ISSN 0004-5411.
• [38] Reynolds, J. C.: Separation Logic: A Logic for Shared Mutable Data Structures, Proc. IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Los Alamitos, CA, USA, July 22-25 2002, ISBN 0-7695-1483-9, ISSN 1043-6871.
• [39] Smetsers, S., Barendsen, E., van Eekelen, M. C. J. D., Plasmeijer, R. J.: Guaranteeing Safe Destructive Updates Through a Type System with Uniqueness Information for Graphs, Dagstuhl Seminar on Graph Transformations in Computer Science, 776, Springer-Verlag, 1994.
• [40] Smith, F., Walker, D., Morrisett, G.: Alias Types, Proc. European Symposium on Programming (ESOP), March 2000.
• [41] Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System, Proc. Parallel Architectures and Languages Europe, 1994.
• [42] Vitek, J., Bokowski, B.: Confined Types in Java, Software - Practice and Experience, 31(6), 2001, 507-532.
• [43] Wadler, P.: Linear types can change the world!, Programming Concepts and Methods, April 1990, IFIP TC 2 Working Conference.
• [44] Wadler, P.: There's no substitute for linear logic, 8'th International Workshop on the Mathematical Foundations of Programming Semantics, April 1992.
• [45] Walker, D., Crary, K., Morrisett, G.: Typed Memory Management in a Calculus of Capabilities, ACM Transactions on Programming Languages and Systems, 24(4), July 2000, 701-771.
• [46] Walker, D., Morrisett, G.: Alias Types for Recursive Data Structures, Proc. Workshop on Types in Compilation (TIC), September 2000.