Timothy G. Griffin
ABSTRACT
The programming language Scheme contains the control construct call/cc that allows access to the current continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as-types correspondence, which relates a constructive proof of a formula α to a program of type α, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting “classical programs” —programs of type α, where α holds classically, but not constructively — is illustrated by the definition of conjunctively, disjunctive, and existential types using standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.
- 1.M. Felleisen. The calculi of A~-CS conversion: a syntactic theory of control and state in imperatire higher.order programming languages. PhD thesis, Indiana University, 1987. Technical Report No. 226. Google Scholar
Digital Library
- 2.M. Felleisen and D. Friedman. Control operators, the secd-machine, and the )~-calculus. In Formal Description of Programming Concep~ III, pages 131-141, North-Holland, 1986.Google Scholar
- 3.M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. Reasoning with continuations. In Proceedings of the First Symposium on Logic in Computer Science, pages 131-141, IEEE, 1986.Google Scholar
- 4.M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52(3):205- 237, 1987. Google ScholarDigital Library
- 5.A. Filinski. Declarative continuations: an investigation of duality in programming language semantics. In Summer Conference on Category Theory and Computer Science, Manchester, UK, Springer-Verlag, 1989. to appear in the Lecture Notes in Computer Science. Google ScholarDigital Library
- 6.A. Filinski. Declarative Continuations and Categorical Duality. Master's thesis, University of Copenhagen, Copenhagen, Denmark, August 1989. DIKU Report 89/11, Computer Science Department.Google Scholar
- 7.M. J. Fischer. Lambda calculus schemata, in Proc. A CM Conference on Proving Assertions About Programs, pages 104-109, 1972. SIG- PLAN Notices 7.1. Google ScholarDigital Library
- 8.J. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Volume 7 of Cambridge Tracts in Computer Science, Cambridge University Press, 1989. Google ScholarDigital Library
- 9.R. }. Hindley and .1. Seldin. Introduction to Combinators and A-Calculus. London Mathematical Society Student Tezts, Cambridge University Press, 1986. Google ScholarDigital Library
- 10.W. Howard. The formulae-as-types notion of construction, in J. P. Seldin and J. R. Hind- Icy, editors, To H. B. Curry: Essays on Comb~. natory Logic, Lambda-Calculus, and Formalism, pages 479-490, Academic Press, NY, 1980.Google Scholar
- 11.P. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4), 1964.Google ScholarCross Ref
- 12.P. Landin. The next 700 prograrnmmg languages. Commun. ACM, 9(3):157-166, 1966. Google ScholarDigital Library
- 13.A. R. Meyer and M. Wand. Continuation semantics in typed lambda-calculi (summary). In R. Parikh, editor, Logics of Programs, pages 219- 224, Springer-Verlag, 1985. Lecture Notes in Computer Science, Volume 193. Google ScholarDigital Library
- 14.G. Plotkin. Call-by-name, call-by-value and the A-calculus. Theoretical Computer Science, } :125-159, 1975.Google Scholar
- 15.D. Prawitz. Natural Deduction. Almquist and Wiksell, 1965.Google Scholar
- 16.J. Rees and W. Clinger. The revised3 report on the algorithmic language scheme. SIGPLAN Notices, 21( 12):37-79, 1986. Google ScholarDigital Library
- 17.G. L. Steele. Common Lisp: The Language. Digital Press, Bedford, MA, 1984. Google ScholarDigital Library
- 18.S. Stenlund. Combinators, Lambda-Terms and Proof Theory. D. Reidel, Dordrecht, Holland, 1972.Google Scholar
Index Terms
- A formulae-as-type notion of control
Recommendations
Loop formulas for circumscription
Clark's completion is a simple nonmonotonic formalism and a special case of several nonmonotonic logics. Recently there has been work on extending completion with ''loop formulas'' so that general cases of nonmonotonic logics such as logic programs (...
Formalizing Type Operations Using the “Image” Type Constructor
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Coinductive Axiomatization of Recursive Type Equality and Subtyping
We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via ...
Comments