More Web Proxy on the site http://driver.im/

article

The Theory of Fexprs is Trivial

Author:

Mitchell WandAuthors Info & Claims

Lisp and Symbolic Computation, Volume 10, Issue 3

Pages 189 - 199

https://doi.org/10.1023/A:1007720632734

Published: 01 May 1998 Publication History

Abstract

We provide a very simple model of a reflective facility based on the pure λ-calculus, and we show that its theory of contextual equivalence is trivial: two terms in the language are contextually equivalent iff they are α-congruent.

References

[1]

1. Abadi, Martin and Cardelli, Luca. A theory of primitive objects: Untyped and first-order systems. Information and Computation, 125(2):78-102, March 1996.

Digital Library

[2]

2. Curry, Haskell B., Feys, R., and Seldin, J.P. Combinatory Logic, volume 2. North-Holland, 1972.

[3]

3. Danvy, Olivier and Malmkjær, Karoline. Intensions and extensions in a reflective tower. In Proc. 1988 ACM Symposium on Lisp and Functional Programming, pages 327-341, 1988.

Digital Library

[4]

4. Jefferson, Stanley and Friedman, Daniel P. A simple reflective interpreter. Lisp and Symbolic Computation, 9(2/3):181-202, May/June 1996.

Digital Library

[5]

5. Malenfant, Jacques, Dony, Christophe and Cointe, Pierre. A semantics of introspection in a reflective prototype-based language. Lisp and Symbolic Computation, 9(2/3):153-180, May/June 1996.

Digital Library

[6]

6. McCarthy, John, et al. LISP 1.5 Programmer's Manual. MIT Press, Cambridge, MA, 1965.

Digital Library

[7]

7. Mendhekar, Anurag. Theoretical Aspects of Reflection in Programming Languages. PhD thesis, Indiana University, Bloomington, IN, 1998. to appear.

Digital Library

[8]

8. Meyer, Albert R. Thirteen puzzles in programming logic. In D. Bjørner, editor, Proceedings of the Workshop on Formal Software Development: Combining Specification Methods, Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, May 1984. Springer-Verlag.

[9]

9. Mogensen, Torben Æ. Efficient self-interpretation in lambda calculus. Journal of Functional Programming, 2(3):345-364, July 1992.

[10]

10. Morris, Jr., James H. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, Cambridge, MA, 1968.

[11]

11. Muchnick, Steven and Pleban, Uwe. A semantic comparison of LISP and SCHEME. In Conference Record of the 1980 LISP Conference, 1980.

Digital Library

[12]

12. Muller, Robert. M-LISP: A representation-independent dialect of LISP with reduction semantics. ACM Transactions on Programming Languages and Systems, 14(4):589-616, October 1992.

Digital Library

[13]

13. Plotkin, Gordon D. Call-by-name, call-by-value and the ¿-calculus. Theoretical Computer Science, 1:125- 159, 1975.

[14]

14. Plotkin, Gordon D. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.

[15]

15. Smith, Brian C. Reflection and semantics in Lisp. In Conf. Rec. 11th ACM Symposium on Principles of Programming Languages, pages 23-35, 1984.

Digital Library

[16]

16. Wadsworth, Christopher P. Some unusual ¿-calculus numeral systems. In J. P. Hindley and J. R. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 215-230. Academic Press, New York and London, 1980.

[17]

17. Wand, Mitchell. Specifying the correctness of binding-time analysis. Journal of Functional Programming, 3(3):365-387, July 1993. preliminary version appeared in Conf. Rec. 20th ACM Symp. on Principles of Prog. Lang. (1993), 137-143.

Digital Library

[18]

18. Wand, Mitchell and Friedman, Daniel P. The mystery of the tower revealed: A non-reflective description of the reflective tower. Lisp and Symbolic Computation, 1:11-37, 1988. Reprinted in Meta-Level Architectures and Reflection (P. Maes and D. Nardi, eds.) North-Holland, Amsterdam, 1988, pp. 111-134.

Cited By

Zhang YAmin N(2022)Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursionProceedings of the ACM on Programming Languages10.1145/34986776:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498677
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Farmer W(2018)Incorporating quotation and evaluation into Church's type theoryInformation and Computation10.1016/j.ic.2018.03.001260:C(9-50)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1016/j.ic.2018.03.001
Show More Cited By

Index Terms

The Theory of Fexprs is Trivial

Recommendations

Contextual isomorphisms
POPL '17

What is the right notion of "isomorphism" between types, in a simple type theory? The traditional answer is: a pair of terms that are inverse up to a specified congruence. We firstly argue that, in the presence of effects, this answer is too liberal and ...
Contextual isomorphisms
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

What is the right notion of "isomorphism" between types, in a simple type theory? The traditional answer is: a pair of terms that are inverse up to a specified congruence. We firstly argue that, in the presence of effects, this answer is too liberal and ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Lisp and Symbolic Computation

Lisp and Symbolic Computation Volume 10, Issue 3

May 1998

82 pages

ISSN:0892-4635

Editors:
Robert R. Kessler
Univ. of Utah, Salt Lake City
,
Carolyn Talcott
Stanford Univ., Stanford

Issue’s Table of Contents

Copyright © Copyright © 1998 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 May 1998

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang YAmin N(2022)Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursionProceedings of the ACM on Programming Languages10.1145/34986776:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498677
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Farmer W(2018)Incorporating quotation and evaluation into Church's type theoryInformation and Computation10.1016/j.ic.2018.03.001260:C(9-50)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1016/j.ic.2018.03.001
Kavvos G(2017)On the Semantics of IntensionalityProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_32(550-566)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_32
Kameyama YKiselyov OShan C(2015)Combinators for impure yet hygienic code generationScience of Computer Programming10.1016/j.scico.2015.08.007112:P2(120-144)Online publication date: 15-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.08.007
Larmuseau APatrignani MClarke D(2015)A High-Level Model for an Assembly Language Attacker by Means of ReflectionProceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications - Volume 940910.1007/978-3-319-25942-0_11(168-182)Online publication date: 4-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-319-25942-0_11
Larmuseau APatrignani MClarke DRusso ATripp O(2014)Operational Semantics for Secure InteroperationProceedings of the Ninth Workshop on Programming Languages and Analysis for Security10.1145/2637113.2637118(40-52)Online publication date: 28-Jul-2014
https://dl.acm.org/doi/10.1145/2637113.2637118
Zhu KDantas DFisher KJia LMandelbaum YPai VWalker DPorto ALópez-Fraguas F(2009)Language support for processing distributed ad hoc dataProceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming10.1145/1599410.1599440(243-254)Online publication date: 7-Sep-2009
https://dl.acm.org/doi/10.1145/1599410.1599440
Stump A(2009)Directly reflective meta-programmingHigher-Order and Symbolic Computation10.1007/s10990-007-9022-022:2(115-144)Online publication date: 1-Jun-2009
https://dl.acm.org/doi/10.1007/s10990-007-9022-0
Culpepper RFelleisen MConsel CLawall J(2007)Debugging macrosProceedings of the 6th international conference on Generative programming and component engineering10.1145/1289971.1289994(135-144)Online publication date: 1-Oct-2007
https://dl.acm.org/doi/10.1145/1289971.1289994
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents