M-LISP: its natural semantics and equational logic
References
[1]
D. Adams. Recognizing quote deemed harmful to eval's laziness. Private communication, 1987.
[2]
J. Backus. Can programming be liberated from the yon Neumann style? A functional style and its algebra of programs. CACM, 21, No 8:613- 641, 1978.
[3]
H. Barendregt. The Lambda Calculus -- Its Syntax and Semantics. North Holland Press, Amsterdam, 1984.
[4]
A. Bawden. Reification without evaluation. In Proceedings o} the A CM Symposium on LISP and Functional Programming, pages 342-351, 1988.
[5]
R. Boyer and J. Moore. Proving theorems about LISP functions. Journal o} the A CM, 22:129- 144, 1975.
[6]
R. Cartwright. User defined data types as an aid to verifying lisp programs. In Automata, Languages and Programming. Edinburgh University Press, 1976.
[7]
O. Danvy and K. Malmkjaer. Intensions and extensions in a reflective tower. In Proceedings of the A CM Symposium on LISP and Functional Programming, pages 327-341, 1988.
[8]
J. des Rivi~res and B. Smith. The implementation of procedurally reflective languages. In Proceedings of the A CM Symposium on LISP and Functional Programming, pages 331-347, 1984.
[9]
M. Felleisen. The theory and practice of first class prompts. In Proceedings of the Fifteenth A C~1 Symposium on Principles of Programming Languages, pages 180-190, 1988.
[10]
M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. Reasoning with continuations. In First Annual Symposium on Logic in Computer Science, pages 131-141, 1986.
[11]
D. Friedman and M. Wand. Reification: Reflection without metaphysics. In Proceedings 6 the A CM Symposium on LISP and Functional Program, vn, lng, pe~~~ 848--055, 1084.
[12]
D. Friedman and M. Wand. The mystery of the tower revealed: A non-reflective description of the reflective tower. In Proceedings of the A CM Symposium on LISP and Functional Programming, pages 298-307, 1986.
[13]
M. Gordon. Operational reasoning and denotational semantics. Technical Report AIM-264, Stanford University, 1975.
[14]
J. Klop and R. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80, No. 2:97-113, 1989.
[15]
E. Kohlbecker and M. Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In Proceedings of the Fourteenth ACM Symposium on Principles of Programming Languages, pages 77-84, 1987.
[16]
I. Mason. Equivalence of first order LISP programs" proving properties of destructive programs via transformations. In First Annual Symposium on Logic in Computer Science, pages 105-117, 1986.
[17]
J. McCarthy. Recursive functions of symbolic expressions and their computation by machine. Communications of the A CM, pages 184-195, 1960.
[18]
J. McCarthy. LISP 1.5 Programer's Manual. MIT Press, 1962.
[19]
S. Muchnick and U. Pleban. A semantic comparison of LISP and Scheme. In Proceedings of the A CM Symposium on LISP and Functional Programming, pages 56-657 1980.
[20]
I. Mason and C. Talcott. Axiomatizing operational equivalence in the presence of side effects. in Fourth Annual Symposium on Logic in Com. puter Science, pages 284-293, 1989.
[21]
R. Muller. MetaLISP: A Representation Independent Dialect of LISP with Reduction Semantics. Phi5 thesis, Boston University, 1989.
[22]
R. Muller. Syntax macros in M-LISP: A representation independent dialect of LISP with reduction semantics. Technical Report CRCT TR-04-90, Harvard University, 1990.
[23]
K. Pitman. Special forms in LISP. In Proceedings o/the A CM Symposium on LISP and Functional Programming, pages 179-187, 1980.
[24]
F. Pfenning and P. Lee. LEAP: A language with eval and polymorphism. In Tapso}t, 1988.
[25]
G. Plotkin. Call-by-name, call-by-value and the A-calculus. Theoretical Computer Science, 1:125- 159, 1975.
[26]
G. Plotkln. A structural approach to operational semantics. Technical Report DAIMI FN- 19, Aarhus University, Denmark, 1981.
[27]
G. Revesz. A llst oriented extension of the Church-Rosser theorem. Technical Report RC 13620 (No. 60941), IBM T. J. Watson Research Center, 198g.
[28]
B. Rosen. Tree manipulation systems and Church-Rosser theorems. Journal of the A CM, 20:160-187, 1973.
[29]
B. Smith. Reflection and Semantics in a Procedural Language. PhD thesis, Massachusetts Institute of Technology, 1982.
[30]
B. Smith. Reflection and semantics in LISP. In Proceedings of the Eleventh ACM Symposium on Principles of Programming Languages, pages 23- 35, 1984.
[31]
P. Wadler. A critique of Abelson and Sussman or why calculating is better than scheming. Sigplan Notices, 22, No. 3:83-94, 1987.
Index Terms
- M-LISP: its natural semantics and equational logic
Recommendations
M-LISP: a representation-independent dialect of LISP with reduction semantics
In this paper we introduce M-LISP, a dialect of LISP designed with an eye toward reconciling LISP's metalinguistic power with the structural style of operational semantics advocated by Plotkin [28]. We begin by reviewing the original definition of LISP [...
Intuitionistic Trilattice Logics
We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN3 introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp
ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an "industrial strength" programming language ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sept. 1991
333 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/115866
- Editor:
- Richard L. Wexelblat
Copyright © 1991 ACM.
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
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 421Total Downloads
- Downloads (Last 12 months)78
- Downloads (Last 6 weeks)14
Reflects downloads up to 15 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in