A formulae-as-type notion of control

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A formulae-as-type notion of control

Full text

Pdf (1.05 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

San Francisco, California, United States

Pages: 47 - 58

Year of Publication: 1989

ISBN:0-89791-343-4

Author

Timothy G. Griffin

Departamento de Ciência da Computação, IMECC - UNICAMP, Caixa Postal, 6065, 13801 Campinas SP, Brazil and Department of Computer Science, Rice University, Houston, TX

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 55, Citation Count: 65

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/96709.96714 What is a DOI?

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 &agr; to a program of type &agr;, 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 &agr;, where &agr; 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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Matthias Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, 1987
	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.
	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.
	4	M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
	5	Andrzej Filinski, Declarative Continuations: an Investigation of Duality in Programming Language Semantics, Category Theory and Computer Science, p.224-249, September 05-08, 1989
	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.
	7	Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
	8	Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
	9	J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
	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.
	11	P. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4), 1964.
	12	P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
	13	Albert R. Meyer , Mitchell Wand, Continuation Semantics in Typed Lambda-Calculi (Summary), Proceedings of the Conference on Logic of Programs, p.219-224, June 17-19, 1985
	14	G. Plotkin. Call-by-name, call-by-value and the A-calculus. Theoretical Computer Science, } :125-159, 1975.
	15	D. Prawitz. Natural Deduction. Almquist and Wiksell, 1965.
	16	J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
	17	Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
	18	S. Stenlund. Combinators, Lambda-Terms and Proof Theory. D. Reidel, Dordrecht, Holland, 1972.

CITED BY 65

	Andrzej Filinski, Linear continuations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-38, January 19-22, 1992, Albuquerque, New Mexico, United States
	Julia L. Lawall , Olivier Danvy, Separating stages in the continuation-passing style transformation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.124-136, March 1993, Charleston, South Carolina, United States
	Hayo Thielecke, From control effects to typed continuation passing, ACM SIGPLAN Notices, v.38 n.1, p.139-149, January 2003
	C.-H. L. Ong , C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.215-227, January 15-17, 1997, Paris, France
	Olivier Danvy , Julia L. Lawall, Back to direct style II: first-class continuations, ACM SIGPLAN Lisp Pointers, v.V n.1, p.299-310, Jan. 1992
	Bruce Duba , Robert Harper , David MacQueen, Typing first-class continuations in ML, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 21-23, 1991, Orlando, Florida, United States
	Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States
	Claudia Faggian, A term calculus for unitary approach to normalization, ACM SIGPLAN Notices, v.34 n.1, p.347, Jan. 1999
	Susumu Hayashi , Ryosuke Sumitomo , Ken-ichiro Shii, Towards the animation of proofs---testing proofs by examples, Theoretical Computer Science, v.272 n.1-2, p.177-195, February 6, 2002
	Yukiyoshi Kemeyama , Masahiko Sato, Strong normalizability of the non-deterministic catch/throw calculi, Theoretical Computer Science, v.272 n.1-2, p.223-245, February 6, 2002
	Dorai Sitaram , Matthias Felleisen, Reasoning with continuations II: full abstraction for models of control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.161-175, June 27-29, 1990, Nice, France
	Gilles Barthe , Tarmo Uustalu, CPS translating inductive and coinductive types, ACM SIGPLAN Notices, v.37 n.3, p.131-142, March 2002
	John Hatcliff , Olivier Danvy, A generic account of continuation-passing styles, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.458-471, January 16-19, 1994, Portland, Oregon, United States
	Hayo Thielecke, Continuations, functions and jumps, ACM SIGACT News, v.30 n.2, June 1999
	Chiyan Chen , Hongwei Xi, Implementing typeful program transformations, ACM SIGPLAN Notices, v.38 n.10, p.20-28, October 2003
	Zena M. Ariola , Hugo Herbelin , Amr Sabry, A type-theoretic foundation of continuations and prompts, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Philip Wadler, Call-by-value is dual to call-by-name, ACM SIGPLAN Notices, v.38 n.9, p.189-201, September 2003
	Carsten Führmann , Hayo Thielecke, On the call-by-value CPS transform and its semantics, Information and Computation, v.188 n.2, p.241-283, 29 January 2004
	Emmanuel Beffara , Vincent Danos, Disjunctive normal forms and local exceptions, ACM SIGPLAN Notices, v.38 n.9, p.203-211, September 2003
	Ken-etsu Fujita, An interpretation of λµ-calculus in λ-calculus, Information Processing Letters, v.84 n.5, p.261-264, 16 December 2002
	Dan Dougherty , Silvia Ghilezan , Pierre Lescanne, Characterizing strong normalization in a language with control operators, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.155-166, August 24-26, 2004, Verona, Italy
	C. Raffalli, Getting results from programs extracted from classical proofs, Theoretical Computer Science, v.323 n.1-3, p.49-70, 14 September 2004
	Hayo Thielecke, Frame rules from answer types for code pointers, ACM SIGPLAN Notices, v.41 n.1, p.309-319, January 2006
	Jean-Louis Krivine, Dependent choice, 'quote' and the clock, Theoretical Computer Science, v.308 n.1-3, p.259-276, 3 November 2003
	Dariusz Biernacki , Olivier Danvy , Chung-chieh Shan, On the static and dynamic extents of delimited continuations, Science of Computer Programming, v.60 n.3, p.274-297, May 2006
	Yukiyoshi Kameyama, Axioms for control operators in the CPS hierarchy, Higher-Order and Symbolic Computation, v.20 n.4, p.339-369, December 2007
	Zena M. Ariola , Hugo Herbelin , Amr Sabry, A proof-theoretic foundation of abortive continuations, Higher-Order and Symbolic Computation, v.20 n.4, p.403-429, December 2007
	Jean-Louis Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, v.20 n.3, p.199-207, September 2007
	Healfdene Goguen , Jean Goubault-Larrecq, Sequent combinators: a Hilbert system for the lambda calculus, Mathematical Structures in Computer Science, v.10 n.1, p.1-79, February 2000
	Peter Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, v.11 n.2, p.207-260, April 2001
	Satoshi Ikeda , Koji Nakazawa, Strong normalization proofs by CPS-translations, Information Processing Letters, v.99 n.4, p.163-170, 31 August 2006
	Nikos Tzevelekos, Investigations on the Dual Calculus, Theoretical Computer Science, v.360 n.1, p.289-326, 21 August 2006
	Gianluigi Bellin , Martin Hyland , Edmund Robinson , Christian Urban, Categorical proof theory of classical propositional calculus, Theoretical Computer Science, v.364 n.2, p.146-165, 6 November 2006
	Riccardo Pucella, Alternative Logics: a book review: SIGACT news logic column 18, ACM SIGACT News, v.38 n.2, June 2007
	Sam Tobin-Hochstadt , Matthias Felleisen, The design and implementation of typed scheme, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Martin Hyland , Paul Blain Levy , Gordon Plotkin , John Power, Combining algebraic effects with continuations, Theoretical Computer Science, v.375 n.1-3, p.20-40, May, 2007
	Magorzata Biernacka , Olivier Danvy, A syntactic correspondence between context-sensitive calculi and abstract machines, Theoretical Computer Science, v.375 n.1-3, p.76-108, May, 2007
	Christopher J. Dutchyn, Specializing continuations a model for dynamic join points, Proceedings of the 6th workshop on Foundations of aspect-oriented languages, p.45-57, March 13-13, 2007, Vancouver, British Columbia, Canada
	Hongwei Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, v.17 n.2, p.215-286, March 2007
	Chiyan Chen , Rui Shi , Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, v.69 n.1-2, p.103-121, January 2006
	C. Urban , G. M. Bierman, Strong Normalisation of Cut-Elimination in Classical Logic, Fundamenta Informaticae, v.45 n.1-2, p.123-155, January 2001
	Daniel J. Dougherty , Silvia Ghilezan , Pierre Lescanne, Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage, Theoretical Computer Science, v.398 n.1-3, p.114-128, May, 2008
	Atsushi Ohori, A proof theory for machine code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.36-es, October 2007
	Philippe De Groote, An environment machine for the λμ-calculus, Mathematical Structures in Computer Science, v.8 n.6, p.637-669, December 1998
	R. David , G. Mounier, An intuitionistic λ-calculus with exceptions, Journal of Functional Programming, v.15 n.1, p.33-52, January 2005
	John Hatcliff , Olivier Danvy, Thunks and the λ-calculus, Journal of Functional Programming, v.7 n.3, p.303-319, May 1997
	Tristan Crolard, A confluent λ-calculus with a catch/throw mechanism, Journal of Functional Programming, v.9 n.6, p.625-647, November 1999
	Th. Streicher , B. Reus, Classical logic, continuation semantics and abstract machines, Journal of Functional Programming, v.8 n.6, p.543-572, November 1998
	Hayo Thielecke, Comparing Control Constructs by Double-Barrelled CPS, Higher-Order and Symbolic Computation, v.15 n.2-3, p.141-160, September 2002
	Gilles Barthe , John Hatcliff , Morten Heine B. Sørensen, CPS Translations and Applications: The Cube and Beyond, Higher-Order and Symbolic Computation, v.12 n.2, p.125-170, September 1999
	Ian A. Mason, Computing with Contexts, Higher-Order and Symbolic Computation, v.12 n.2, p.171-201, September 1999
	Hayo Thielecke, Using a Continuation Twice and Its Implications for the Expressive Power of call/cc, Higher-Order and Symbolic Computation, v.12 n.1, p.47-73, April 1999
	John C. Reynolds, Definitional Interpreters Revisited, Higher-Order and Symbolic Computation, v.11 n.4, p.355-361, December 1998
	Hugo Herbelin , Silvia Ghilezan, An approach to call-by-name delimited continuations, ACM SIGPLAN Notices, v.43 n.1, January 2008
	David Van Horn , Harry G. Mairson, Relating complexity and precision in control flow analysis, ACM SIGPLAN Notices, v.42 n.9, September 2007
	René David , Karim Nour, Arithmetical Proofs of Strong Normalization Results for Symmetric λ-calculi, Fundamenta Informaticae, v.77 n.4, p.489-510, December 2007
	Zena m. Ariola , Hugo Herbelin, Control reduction theories: The benefit of structural substitution, Journal of Functional Programming, v.18 n.3, p.373-419, May 2008
	Steffen Van bakel , Pierre Lescanne, Computation with classical sequents, Mathematical Structures in Computer Science, v.18 n.3, p.555-609, June 2008
	Olivier Danvy, Defunctionalized interpreters for programming languages, ACM SIGPLAN Notices, v.43 n.9, p.131-142, September 2008
	Vladimir Komendantsky, Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), 225, p.161-179, January, 2009
	Jason Reed , Frank Pfenning, Intuitionistic Letcc via Labelled Deduction, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.91-111, March, 2009
	Hayo Thielecke, Control effects as a modality, Journal of Functional Programming, v.19 n.1, p.17-26, January 2009
	Stefano Guerrini , Andrea Masini, Proofs, tests and continuation passing style, ACM Transactions on Computational Logic (TOCL), v.10 n.2, p.1-34, February 2009
	Zena M. Ariola , Aaron Bohannon , Amr Sabry, Sequent calculi and abstract machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.4, p.1-48, May 2009
	Małgorzata Biernacka , Dariusz Biernacki, A Context-based Approach to Proving Termination of Evaluation, Electronic Notes in Theoretical Computer Science (ENTCS), 249, p.169-192, August, 2009