article

Free access

Is there a use for linear logic?

Author:

Philip WadlerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 26, Issue 9

Pages 255 - 273

https://doi.org/10.1145/115866.115894

Published: 01 May 1991 Publication History

PDF eReader

References

[1]

S. Abramsky, Computational interpretations of linear logic. Preprint, Imperial College, London.

Google Scholar

[2]

A. Bloss, Path analysis: using orderof-evaluation information to optimize lazy functional languages. Ph.D. thesis, Yale University, Department of Computer Science, 1989.

Google Scholar

[3]

J. Darlington and R. M. Burstall, A system which automatically improves programs. Acta Informatica, 6:41-60, 1976.

Digital Library

Google Scholar

[4]

L. Damns and I{. Milner, Principal type schemes for functional programs. In Proceedings 9'th A CM Symposium on Principles of Programming Languages, Albuquerque, N.M., January 1982.

Digital Library

Google Scholar

[5]

J.-Y. Girard, Linear logic. Theoretical Compuler Science, 50:1-102, 1987.

Digital Library

Google Scholar

[6]

J.-Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types. Cambridge University Press, 1989.

Digital Library

Google Scholar

[7]

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.

Google Scholar

[8]

R. Hindley, The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc., 146:29-60, December 1969.

Google Scholar

[9]

S. HolmstrSm, A linear functional language. Draft paper, Chalmers University of Technology, 1988.

Google Scholar

[10]

P. Hudak, A semantic model of reference counting and its abstraction. In Proceedings A CM Conference on Lisp and Functional Programming, August 1986.

Digital Library

Google Scholar

[11]

T.-M. Kuo and P. Mishra, Stricthess analysis: a new perspective based on type inference. In Proceedings 4'th International Conference on Functional Programming Languages and Computer Architecture, ACM Press, London, September 1989.

Digital Library

Google Scholar

[12]

Y. Lafont, The linear abstract machine. Theoretical Computer Science, 59:157-180, 1988.

Digital Library

Google Scholar

[13]

P~. Milner, A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17:348-375, 1978.

Crossref

Google Scholar

[14]

J. C. Mitchell, Coercion and type inference. In Proceedings 11 'th A CM Symposium on Principles of Programming Languages, January 1984.

Digital Library

Google Scholar

[15]

J. C. Mitchell, Extending Curry and ML type inference with subtypes. Preprint. To appear in Journal of Functional Programming, 1(3), June 1991.

Crossref

Google Scholar

[16]

D. A. Schmidt, Detecting global variables in denotational specifications. A CM Trans. on Programming Languages and Systems, 7:299-310, 1985. (Also Internal Report CSR-143, Computer Science Department, University of Edinburgh, September 1983.)

Digital Library

Google Scholar

[17]

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.

Google Scholar

[18]

D. Wakeling, Linearity and laziness. Ph.D. dissertation, University of York, November 1990.

Digital Library

Google Scholar

[19]

D. A. Wright, Strictness analysis via type inference. Technical report, University of Tasmania, September 1989.

Google Scholar

Cited By

View all

Antonelli MDal Lago UPistone P(2023)Towards logical foundations for probabilistic computationAnnals of Pure and Applied Logic10.1016/j.apal.2023.103341(103341)Online publication date: Jul-2023
https://doi.org/10.1016/j.apal.2023.103341
McBride C(2016)I Got Plenty o’ Nuttin’A List of Successes That Can Change the World10.1007/978-3-319-30936-1_12(207-233)Online publication date: 25-Mar-2016
https://doi.org/10.1007/978-3-319-30936-1_12
Hua B(2011)Static typing for a substructural lambda calculusFrontiers of Computer Science in China10.1007/s11704-011-9106-15:3(369-380)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1007/s11704-011-9106-1
Show More Cited By

Index Terms

Is there a use for linear logic?
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
A Paraconsistent Linear-time Temporal Logic

Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...
The decidability of the intensional fragment of classical linear logic

Intensional classical linear logic (MELL) is proved decidable.Intensional interlinear logic (RLL) is proved decidable.We adapt Kripke's method used to prove decidability for some relevance logics.The semi-relevant RLL emerges as a logic superior to MELL ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 26, Issue 9

Sept. 1991

333 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/115866

Editor:
Richard L. Wexelblat
IDA/CSED, Alexandria, VA

Issue’s Table of Contents

PEPM '91: Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation
May 1991
333 pages
ISBN:0897914333
DOI:10.1145/115865
Chairmen:
Charles Consel,
Olivier Danvy

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1991

Published in SIGPLAN Volume 26, Issue 9

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

68
Total Citations
View Citations
816
Total Downloads

Downloads (Last 12 months)119
Downloads (Last 6 weeks)17

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Antonelli MDal Lago UPistone P(2023)Towards logical foundations for probabilistic computationAnnals of Pure and Applied Logic10.1016/j.apal.2023.103341(103341)Online publication date: Jul-2023
https://doi.org/10.1016/j.apal.2023.103341
McBride C(2016)I Got Plenty o’ Nuttin’A List of Successes That Can Change the World10.1007/978-3-319-30936-1_12(207-233)Online publication date: 25-Mar-2016
https://doi.org/10.1007/978-3-319-30936-1_12
Hua B(2011)Static typing for a substructural lambda calculusFrontiers of Computer Science in China10.1007/s11704-011-9106-15:3(369-380)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1007/s11704-011-9106-1
Baillot PHofmann MKutsia TSchreiner WFernández M(2010)Type inference in intuitionistic linear logicProceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming10.1145/1836089.1836118(219-230)Online publication date: 26-Jul-2010
https://dl.acm.org/doi/10.1145/1836089.1836118
de Vries EPlasmeijer RAbrahamson D(2008)Uniqueness Typing SimplifiedImplementation and Application of Functional Languages10.1007/978-3-540-85373-2_12(201-218)Online publication date: 2008
https://doi.org/10.1007/978-3-540-85373-2_12
Berdine JO'Hearn P(2006)Strong Update, Disposal, and Encapsulation in Bunched TypingElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2006.04.006158(81-98)Online publication date: 1-May-2006
https://dl.acm.org/doi/10.1016/j.entcs.2006.04.006
Reddy U(1997)Global State Considered Unnecessary: Introduction to Object-Based SemanticsAlgol-like Languages10.1007/978-1-4757-3851-3_9(227-295)Online publication date: 1997
https://doi.org/10.1007/978-1-4757-3851-3_9
Reddy U(1996)Global state considered unnecessary: An introduction to object-based semanticsLisp and Symbolic Computation10.1007/BF018060329:1(7-76)Online publication date: Feb-1996
https://doi.org/10.1007/BF01806032
Odersky MRabin DHudak PVan Deusen MLang B(1993)Call by name, assignment, and the lambda calculusProceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/158511.158521(43-56)Online publication date: 1-Mar-1993
https://dl.acm.org/doi/10.1145/158511.158521
Bertram NLai THsu J(2024)Verifying Cake-Cutting, FasterComputer Aided Verification10.1007/978-3-031-65630-9_6(109-129)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_6
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Index Terms

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

A Paraconsistent Linear-time Temporal Logic

The decidability of the intensional fragment of classical linear logic

Comments

Information

Published In

Publisher

Publication History

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations