Hostname: page-component-76fb5796d-wq484 Total loading time: 0 Render date: 2024-04-26T01:09:03.063Z Has data issue: false hasContentIssue false
  • English
  • Français

Lilac: a functional programming language based on linear logic

Part of: JFP Research Articles

Published online by Cambridge University Press:  07 November 2008

Ian Mackie
Ian Mackie
Affiliation:
Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ, UK (E-mail: im@doc.ic.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation and examples of use.

Type
Articles
Information
Journal of Functional Programming , Volume 4 , Issue 4 , October 1994 , pp. 395 - 433
Copyright
Copyright © Cambridge University Press 1994

References

Abadi, M., Cardelli, L., Curien, P.-L. & Lévy, J.-J. (1991) Explicit substitutions. Journal of Functional Programming 1(4), 375–416.Google Scholar
Abramsky, S. (1993) Computational Interpretation of Linear Logic. Theoretical Computer Science 111, 3–57. (Earlier version appeared as Imperial College Technical Report DOC 90/20, October 1990.)Google Scholar
Abramsky, S. & Hankin, C. (Eds.) (1987) Abstract Interpretation for Declarative Languages. Ellis Horwood.Google Scholar
Benton, N., Bierman, G., de Paiva, V. & Hyland, M. (1992) Term assignment for intuitionistic linear logic. Technical Report No. 262, University of Cambridge.Google Scholar
Bierman, G. (1992) Type systems, linearity and functional programming. Slides from talk given at CLICS Workshop Aarhus University, Denmark.Google Scholar
Boudol, G. (1993) The lambda-calculus with multiplicities. Preliminary report, INRIA-Sophia Antipolis.CrossRefGoogle Scholar
Burstall, R. & Darlington, J. (1977) A transformation system for developing recursive programs. Journal ACM 24(1), 44–67.Google Scholar
Chirimar, J., Gunter, C. & Rieke, J. (1991), Proving memory management invariants for a language based on linear logic, Technical report, University of Pennsylvania, Department of Computer and Information Science.CrossRefGoogle Scholar
Damas, L. (1985) Type Assignment in Programming Languages. PhD thesis, University of Edinburgh.Google Scholar
Damas, L. & Milner, R. (1982) Principal type schemes for functional programs. In: Conference Record of the Ninth Annual ACM Symposium on the Principles of Programming Languages, pp. 207–212.Google Scholar
Field, A. & Harrison, P. (1988) Functional Programming. Addison Wesley.Google Scholar
Girard, J.-Y. (1987) Linear Logic. Theoretical Computer Science 50(1), 1–102.Google Scholar
Girard, J.-Y. (1989) Towards a geometry of interaction. In: Gray, J. & Scedrov, A. (Eds.), Categories in Computer Science and Logic: Vol. 92 of Contemporary Mathematics, American Mathematical Society, pp. 69–108.Google Scholar
Girard, J.-Y., Lafont, Y. & Taylor, P. (1989) Proofs and Types. Vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
Gonthier, G., Abadi, M. & Lévy, J.-J. (1992) The geometry of optimal lambda reduction. In: Proceedings of ACM Symposium Principles of Programming Languages, pp. 15–26.CrossRefGoogle Scholar
Henderson, P. (1980) Functional Programming: Applications and Implementation. Prentice Hall.Google Scholar
Holmström, S. (1988) Linear functional programming. In: Johnsson, T., Peyton Jones, S. & Karlsson, K. (Eds.), Proceedings of the Workshop on Implementation of Lazy Functional Languages, pp. 13–32.Google Scholar
Lafont, Y. (1988 a) Introduction to linear logic. Lecture Notes for the Summerschool on Constructive Logics and Category Theory, Isle of Thorns.Google Scholar
Lafont, Y. (1988b) Logiques, Catégories and Machines. PhD thesis, Université de Paris 7.Google Scholar
Lincoln, P. (1992) Linear logic. ACM SIGACT Notices 23(2) 29–37.CrossRefGoogle Scholar
Lincoln, P. & Mitchell, J. (1992) Operational aspects of linear lambda calculus. In: Proceedings 7th IEEE Symposium Logic in Computer Science,Santa Cruz, CA.Google Scholar
Mackie, I. (1991) Lilac: A functional programming language based on linear logic. Master's thesis, Imperial College of Science, Technology and Medicine, University of London.Google Scholar
Mackie, I., Román, L. & Abramsky, S. (1993) An internal language for autonomous categories. Journal of Applied Categorical Structures Vol. 1 pp. 311–343.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. Journal of Computer and System Sciences.CrossRefGoogle Scholar
Milner, R., Tofte, M. & Harper, R. (1990) The Definition of Standard ML. MIT Press.Google Scholar
O'Hearn, P. W. (1991) Linear logic and inference control (preliminary report). In: Proceedings 4th Category Theory and Computer Science conference, pp. 74–93.Google Scholar
Peyton Jones, S. (1987) The Implementation of Functional Programming Languages. Prentice-Hall.Google Scholar
Plotkin, G. (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University.Google Scholar
Robinson, J. A. (1965) A machine-oriented logic based on the resolution principle. Journal ACM 12(1) 23–11.CrossRefGoogle Scholar
Roversi, L. (1992) A compiler from curry-typed-λ-terms to the linear-λ-terms. In: Proceedings of the IV Convegno italiano di informatica teorica,World Scientific (to appear).Google Scholar
Scedrov, A. (1993) A brief guide to linear logic. In: Rozenberg, G. & Salomaa, A. (Eds), Current Trends in Theoretical Computer Science. World Scientific.Google Scholar
Turner, R. (1991) Constructive foundations for Functional Programming. McGraw Hill.Google Scholar
Wadler, P. (1990) Linear types can change the world! In: Broy, M. & Jones, C. (Eds.), Programming Concepts and Methods. IFIP TC2 Working Conference on Programming Concepts and Methods, North-Holland, Sea of Galilee, Israel.Google Scholar
Wadler, P. (1991) Is there a use for linear logic? In: Conference on Partial Evaluation and Semantics-Based Program Manipulation (PEPM).ACM Press,New Haven, CT.Google Scholar
Wadler, P. (1992) There's no substitute for linear logic. Presented at Workshop on Mathematical Foundations of Programming Language Semantics.Google Scholar
Wadler, P. (1993) A taste of linear logic. Mathematical Foundations of Computer Science, Gdansk. Springer-Verlag.Google Scholar
Wakeling, D. (1990) Linearity and Laziness. PhD thesis, University of York.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.