Abstract
We describe the core of a new strongly-typed functional programming language called LEAP, a “Language with Eval And Polymorphism.” Pure LEAP is an extension of the ω-order polymorphic λ-calculus (F ω) by global definitions that allows the representation of programs and the definition of versions of reify, reflect, and eval for all of (F ω). Pure LEAP is therefore highly reflexive and strongly typed. We believe that Pure LEAP can be extended to a practical and efficient metalanguage in the ML tradition. At present we are experimenting with a prototype implementation of Pure LEAP.
This research was supported in part by the Office of Naval Research under contract N00014-84-K-0415 and in part by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 5404, monitored by the Office of Naval Research under the same contract.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed Λ-programs on term algebras. Theoretical Computer Science, 39:135–154, 1985.
Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, Princeton, New Jersey, 1941.
Mitchell D. Wand and Daniel P. Friedman. The mystery of the tower revealed: a non-reflective description of the reflective tower. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, Cambridge, pages 198–307, ACM, August 1986.
Daniel P. Friedman and Mitchell Wand. Reification: reflection without metaphysics. In Proceedings of the 1984 ACM Symposium on Lisp and Functional Programming, pages 348–355, ACM Press, August 1984.
Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordere supérieur. PhD thesis, Université Paris VII, 1972.
Jean-Yves Girard. Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92, North-Holland Publishing Co., Amsterdam, London, 1971.
David B. MacQueen. References and weak polymorphism. 1988. Standard ML of New Jersey compiler release notes.
John McCarthy. History of LISP. ACM SIGPLAN Notices, 13(8):217–223, August 1978.
John McCarthy, Paul W. Abrahams, Daniel J. Edwards, Timothy P. Hart, and Michael I. Levin. LISP 1.5 Programmer's Manual. MIT Press, Cambridge, 1962.
Dale A. Miller and Gopalan Nadathur. Higher-order logic programming. In Proceedings of the Third International Conference on Logic Programming, Springer Verlag, July 1986.
Robin Milner. The Standard ML core language. Polymorphism, II(2), October 1985. Also Technical Report ECS-LFCS-86-2, University of Edinburgh, Edinburgh, Scotland, March 1986.
Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, August 1978.
Frank Pfenning. Inductively Defined Types in the Calculus of Constructions. Ergo Report 88–069, Carnegie Mellon University, Pittsburgh, Pennsylvania, November 1988.
Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, ACM Press, July 1988.
John Reynolds. Three approaches to type structure. In Hartmut Ehrig, Christiane Floyd, Maurice Nivat, and James Thatcher, editors, Mathematical Foundations of Software Development, pages 97–138, Springer-Verlag LNCS 185, March 1985.
John Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, pages 408–425, Springer-Verlag LNCS 19, New York, 1974.
John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the 25th ACM National Conference, pages 717–740, ACM, New York, 1972.
Brian Cantwell Smith. Reflection and Semantics in a Procedural Language. Technical Report MIT-LCS-TR-272, Massachusetts Institute of Technology, Cambridge, Massachusetts, January 1982.
Brian Cantwell Smith. Reflection and semantics in Lisp. In Proceedings of the Eleventh Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, pages 23–35, ACM, January 1984.
Guy Steele and G. Sussman. The Art of the Interpreter, or, The Modularity Complex (Parts Zero, One, and Two). Artificial Intelligence Laboratory Memo AIM-453, Massachusetts Institute of Technology, Cambridge, Massachusetts, 1978.
Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, Edinburgh University, 1987.
Mitchell D. Wand and Daniel P. Friedman. The mystery of the tower revealed: a nonreflective description of the reflective tower. Lisp and Symbolic Computation, 1(1):11–38, June 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pfenning, F., Lee, P. (1989). LEAP: A language with eval and polymorphism. In: Díaz, J., Orejas, F. (eds) TAPSOFT '89. TAPSOFT 1989. Lecture Notes in Computer Science, vol 352. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50940-2_46
Download citation
DOI: https://doi.org/10.1007/3-540-50940-2_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50940-0
Online ISBN: 978-3-540-46118-0
eBook Packages: Springer Book Archive