Is there a use for linear logic?

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Is there a use for linear logic?

Full text

Pdf (1.34 MB)

Source

ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation archive
Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation table of contents

New Haven, Connecticut, United States

Pages: 255 - 273

Year of Publication: 1991

ISBN:0-89791-433-3

Also published in ...

Author

Philip Wadler

Department of Computing Science, University of Glasgow, G12 8QQ, Scotland

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 22, Citation Count: 25

Additional Information:

references cited by index terms collaborative colleagues peer to peer

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/115865.115894 What is a DOI?

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.

	Abr90	S. Abramsky, Computational interpretations of linear logic. Preprint, Imperial College, London.
	Blo89	A. Bloss, Path analysis: using orderof-evaluation information to optimize lazy functional languages. Ph.D. thesis, Yale University, Department of Computer Science, 1989.
	DB76	J. Darlington and R. M. Burstall, A system which automatically improves programs. Acta Informatica, 6:41-60, 1976.
	DM82	Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
	Gir87	Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
	GLT89	Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
	GH90	J. Guzm~n and P. Hudak, Singlethreaded polymorphic lambda calculus. In Proceedings 5'th IEEE Symposium on Logic in Computer Science, Philadelphia, Pa., June 1990.
	Hin69	R. Hindley, The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc., 146:29-60, December 1969.
	Hol88	S. HolmstrSm, A linear functional language. Draft paper, Chalmers University of Technology, 1988.
	Hud86	Paul Hudak, A semantic model of reference counting and its abstraction (detailed summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.351-363, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319876]
	KM89	Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
	Laf88	Y. Lafont, The linear abstract machine, Theoretical Computer Science, v.59 n.1-2, p.157-180, July 1988 [doi>10.1016/0304-3975(88)90100-4]
	Mil78	P~. Milner, A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17:348-375, 1978.
	Mit84	John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
	Mit91	J. C. Mitchell, Extending Curry and ML type inference with subtypes. Preprint. To appear in Journal of Functional Programming, 1(3), June 1991.
	Sch85	David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
	Wad90	P. Wadler, Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland, 1990.
	Wak90	David Wakeling, Linearity and laziness, University of York, York, UK, 1991
	Wri89	D. A. Wright, Strictness analysis via type inference. Technical report, University of Tasmania, September 1989.

CITED BY 25

	Henry G. Baker, Sparse polynomials and linear logic, ACM SIGSAM Bulletin, v.27 n.4, p.10-14, Dec. 1993
	Dana Harrington, Uniqueness logic, Theoretical Computer Science, v.354 n.1, p.24-41, 21 March 2006
	Jörgen Gustavsson, A type based sharing analysis for update avoidance and optimisation, ACM SIGPLAN Notices, v.34 n.1, p.39-50, Jan. 1999
	Henry G. Baker, A “linear logic” Quicksort, ACM SIGPLAN Notices, v.29 n.2, p.13-18, Feb. 1994
	Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States
	Yasuhiko Minamide, A functional representation of data structures with a hole, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.75-84, January 19-21, 1998, San Diego, California, United States
	Chris Hankin , Daniel Le Métayer, Deriving algorithms from type inference systems: application to strictness analysis, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 16-19, 1994, Portland, Oregon, United States
	Jawahar Chirimar , Carl A. Gunter , Jon G. Riecke, Proving memory management invariants for a language based on linear logic, ACM SIGPLAN Lisp Pointers, v.V n.1, p.139-150, Jan. 1992
	Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States
	Guy E. Blelloch , Margaret Reid-Miller, Pipelining with futures, Proceedings of the ninth annual ACM symposium on Parallel algorithms and architectures, p.249-259, June 23-25, 1997, Newport, Rhode Island, United States
	Tyng-Ruey Chuang , Benjamin Goldberg, Real-time deques, multihead Turing machines, and purely functional programming, Proceedings of the conference on Functional programming languages and computer architecture, p.289-298, June 09-11, 1993, Copenhagen, Denmark
	G. M. Bierman, Program equivalence in a linear functional language, Journal of Functional Programming, v.10 n.2, p.167-190, March 2000
	David Aspinall , Adriana Compagnoni, Heap-Bounded Assembly Language, Journal of Automated Reasoning, v.31 n.3-4, p.261-302, 2003
	George Becker , Neil V. Murray, Efficient execution of programs with static semantics, ACM SIGPLAN Notices, v.30 n.4, p.51-60, April 1995
	Henry G. Baker, The Boyer benchmark meets linear logic, ACM SIGPLAN Lisp Pointers, v.VI n.4, p.3-10, Oct.-Dec. 1993
	David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States
	Zena M. Ariola , Amr Sabry, Correctness of monadic state: an imperative call-by-need calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.62-74, January 19-21, 1998, San Diego, California, United States
	Henry G. Baker, Minimizing reference count updating with deferred and anchored pointers for functional data structures, ACM SIGPLAN Notices, v.29 n.9, p.38-43, Sept. 1994
	Naoki Kobayashi , Benjamin C. Pierce , David N. Turner, Linearity and the pi-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.358-371, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Peter O'hearn, On bunched typing, Journal of Functional Programming, v.13 n.4, p.747-796, July 2003
	Peter W. O'Hearn , John C. Reynolds, From Algol to polymorphic linear lambda-calculus, Journal of the ACM (JACM), v.47 n.1, p.167-223, Jan. 2000
	Naoki Kobayashi , Benjamin C. Pierce , David N. Turner, Linearity and the pi-calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.5, p.914-947, Sept. 1999
	Henry G. Baker, Lively linear Lisp: “look ma, no garbage!”, ACM SIGPLAN Notices, v.27 n.8, p.89-98, Aug. 1992
	Henry G. Baker, “Use-once” variables and linear objects: storage management, reflection and multi-threading, ACM SIGPLAN Notices, v.30 n.1, p.45-52, Jan. 1995
	Henry G. Baker, Linear logic and permutation stacks—the Forth shall be first, ACM SIGARCH Computer Architecture News, v.22 n.1, p.34-43, March 1994