Mattias Felleisen
ABSTRACT
An analysis of the λugr;-C-calculus and its problematic relationship to operational equivalence leads to a new control facility: the prompt-application. With the introduction of prompt-applications, the control calculus becomes a traditional calculus all of whose equations imply operational equivalence. In addition, prompt-applications enhance the expressiveness and efficiency of the language. We illustrate the latter claim with examples from such distinct areas as systems programming and tree processing.
- 1.BARENDREGT, H.P. The Lambda Calculus: Its Syntax and Semantics. rev. ed. Studies in Logic and the Foundations of Mathematics 103. North- Holland, Amsterdam, 1984.Google Scholar
- 2.FELLEISEN, M. The Calculi of Lambda-v-CS- Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. Ph.D. dissertation, indiana University, 1987. Google ScholarDigital Library
- 3.FELLEISEN, M., D.P. FRIEDMAN, B. DUBA, AND J. MEKrtILL. Beyond continuations. Technical Report No 216, Indiana University Computer Science Department, 1987.Google Scholar
- 4.FELLEISEN, M., D.P. FRIEDMAN, E. KOHL- BECKER, AND B. DUBA. A syntactic theory of sequential control, Theor. Comput. Sci., 1987, to appear. Google ScholarDigital Library
- 5.HAYNES, C. AND D.P. FRIEDMAN. Embedding continuations in procedural objects. ACM Trans. Program. Lang. Sys$. 9(4), 1987. Google ScholarDigital Library
- 6.HANSON, C., ,}. LAMPING. Dynamic binding in Scheme, unpublished manuscript, 1984, MIT.Google Scholar
- 7.JOHNSON, G.F. GL~A language and environment for interactively experimenting with denotationM definitions. In Proc. SIGPLAN '87 Symposium on In~'erprefers and Interpretive Techniques SIGPLAN .Notices 22(7), 1987, 165-176. Google ScholarDigital Library
- 8.LANDIN, P.J. The next 700 programming languages. Commnn. ACM 9(3), 1966, 157-166. Google ScholarDigital Library
- 9.LANDIN, P.J. The mechanical evaluation of expressions. Compu~. J. 6(4), 1964, 308-320.Google ScholarCross Ref
- 10.MCCARTHY, J. et al. Lisp 1.5 .Programmers Manual. sec. ed. MIT Press, Cambridge, 1965. Google ScholarDigital Library
- 11.PLOTKIN, G.D. Call-by-name, call-by-value, and the A-calculus. Theor. Comput. Sci. 1, 1975, 125-159.Google ScholarCross Ref
- 12.REES J. AND W. CLINGER (Eds.). The reviseda report on the algorithmic language Scheme. SIG- PLAN Notices 21(12), 1986, 37-79. Google ScholarDigital Library
- 13.REYNOLDS, J.C. Definitional interpreters for higher-order programming languages. In Proc. A CM Annual Conference, 1972, 71'7-740. Google ScholarDigital Library
- 14.STEELE, G. Common Lisp--The Language. Digital Press, 1984. Google ScholarDigital Library
Index Terms
- The theory and practice of first-class prompts
Recommendations
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
AbstractWe discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with ...
First-Order Temporal Verification in Practice
First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems ...
Proof Theory for First Order Łukasiewicz Logic
TABLEAUX '07: Proceedings of the 16th international conference on Automated Reasoning with Analytic Tableaux and Related MethodsAn approximate Herbrand theorem is proved and used to establish Skolemization for first-order ï ukasiewicz logic. Proof systems are then defined in the framework of hypersequents. In particular, extending a hypersequent calculus for propositional ï ...
Comments