A Curry-Howard foundation for functional computation with control

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Curry-Howard foundation for functional computation with control

Full text

Pdf (900 KB)

Source

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

Paris, France

Pages: 215 - 227

Year of Publication: 1997

ISBN:0-89791-853-3

Authors

C.-H. L. Ong	Oxford University Computing Laboratory
C. A. Stewart	Oxford University Computing Laboratory

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 26, Citation Count: 20

Additional Information:

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/263699.263722 What is a DOI?

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	Alexander Aiken , Edward L. Wimmers , John H. Williams, Program transformation in the presence of errors, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.210-217, December 1989, San Francisco, California, United States [doi>10.1145/96709.96730]
	2	Franco Barbanera , Stefano Berardi, Extracting Constructive Content from Classical Logic via Control-like Reductions, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.45-59, March 16-18, 1993
	3	H. Barendregt. The Lambda Calculus. North-Holland, revised edition, 1984.
	4	Ulrich Berger , Helmut Schwichtenberg, Program Extraction from Classical Proofs, Selected Papers from the International Workshop on Logical and Computational Complexity, p.77-97, October 13-16, 1994
	5	G. M. Bierman. Towards a classical linear A-calculus. In Proceedings of Tokyo Conference on Linear Logic, volume 3 of Electronic Notes in Computer Science. Elsevier, 1996.
	6	Thierry Coquand, A semantics of evidence for classical arithmetic, Journal of Symbolic Logic, v.60 n.1, p.325-337, March 1995 [doi>10.2307/2275524]
	7	V. Danos, J.-B. Joinet, and H. Schellinx. A new deconstructive logic: linear logic, in J.-Y. Girard et al, editor, Advances in Linear Logic. Cambridge Univ. Press, 1995.
	8	O. Danvy and A. Filinski. Representing control: A study of the CPS transformation. Math. Struct. Comp. Sc., 2(4):361- 391, 1992.
	9	Philippe de Groote, A CPS-Translation of the Lambda-µ-Calculus, Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.85-99, April 11-13, 1994
	10	M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
	11	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]
	12	Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
	13	J.-Y. Girard. A new constructive logic: classical logic. Math. Struct. in Comp. Science, 1:255-296, 1991.
	14	M. J. C. Gordon, A. J. R. Milner, and C. P. Wadsworth. Edinburgh LCF. LNCS 78, Springer-Verlag, 1979.
	15	Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
	16	Carl A. Gunter , Didier Rémy , Jon G. Riecke, A generalization of exceptions and control in ML-like languages, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.12-23, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224173]
	17	R. Harper, B. Dubs, and D. MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465-484, October 1993.
	18	Christopher T. Haynes, Logic continuations, Journal of Logic Programming, v.4 n.2, p.157-176, June 1, 19876 [doi>10.1016/0743-1066(87)90016-1]
	19	Christopher T Haynes , Daniel P Friedman , Mitchell Wand, Obtaining coroutines with continuations, Computer Languages, v.11 n.3-4, p.143-153, 1986 [doi>10.1016/0096-0551(86)90007-X]
	20	M. Hofmann. Sound and complete axiomatisations of callby-value control operators, preprint, 1994.
	21	J.-L. Krivine. Classical logic, storage operators and second order A-calculus. Annals of Pure and Applied Logic, 68:53- 78, 1994.
	22	X. Leroy. The Carol Light System, release 0.6: Documentation and User's Manual. INRIA, 1993. Included in the Caml Light distribution.
	23	Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
	24	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	25	C. Murthy. An evaluation semantics for classical proofs. In Proc. 5th IEEE Annual Symposium on Logic in Computer Science. mEE Computer Society Press, 1991.
	26	H. Nakano. Logical Structure of Catch and Throw Mechanism. PhD thesis, University of Tokyo, 1995.
	27	C. -H. L. Ong, A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.230, July 27-30, 1996
	28	Michel Parigot, Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.190-201, July 15-20, 1992
	29	Michel Parigot, Classical Proofs as Programs, Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory, p.263-276, August 24-27, 1993
	30	M. Parigot. Strong normalization for second order classical natural deduction. In Proc. 8th Annual IEEE Symposium on Logic in Computer Science, pages 39-46. IEEE Computer Society Press, 1993.
	31	Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
	32	G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125-159, 1975.
	33	G. D. Plotkin. LCF as a programming language. Theoretical Computer Science, 5:223-255, 1977.
	34	D. Prawitz. Natural Deduction. Almqvist and Wiksell, 1965. Stockholm Studies in Philosophy 3.
	35	John H. Reppy, Concurrent programming in ML, Cambridge University Press, New York, NY, 1999
	36	Masahiko Sato, Intuitionistic and classical natural deduction systems with the catch and the throw rules, Theoretical Computer Science, v.175 n.1, p.75-92, March 30, 1997
	37	Dana S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, v.121 n.1-2, p.411-440, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90095-B]
	38	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 [doi>10.1145/91556.91626]
	39	C. A. Stewart. Classical prools and a theory of functional control. PhD thesis, PRG, University of Oxford, 1997. In preparation.
	40	T. Streicher and B. Reus. Continuation semantics: control operators and abstract machines. Submitted for publication, 1996.
	41	C. Talcott, Rum. An intensional theory of function and control abstractions, Lecture notes in computer science on Foundations of logic and functional programming, p.3-44, June 1988, Trento, Italy
	42	Judith Lynne Underwood, Aspects of the computational content of proofs, Cornell University, Ithaca, NY, 1994
	43	Mitchell Wand, Continuation-based multiprocessing, Proceedings of the 1980 ACM conference on LISP and functional programming, p.19-28, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802786]

CITED BY 20

	Pierre-Louis Curien , Hugo Herbelin, The duality of computation, ACM SIGPLAN Notices, v.35 n.9, p.233-243, Sept. 2000
	Gilles Barthe , Tarmo Uustalu, CPS translating inductive and coinductive types, ACM SIGPLAN Notices, v.37 n.3, p.131-142, March 2002
	Martin Hofmann , Thomas Streicher, Completeness of continuation models for λµ-calculus, Information and Computation, v.179 n.2, p.332-355, December 15, 2002
	Philip Wadler, Call-by-value is dual to call-by-name, ACM SIGPLAN Notices, v.38 n.9, p.189-201, September 2003
	Emmanuel Beffara , Vincent Danos, Disjunctive normal forms and local exceptions, ACM SIGPLAN Notices, v.38 n.9, p.203-211, September 2003
	Koji Nakazawa, Confluency and strong normalizability of call-by-value λµ-calculus, Theoretical Computer Science, v.290 n.1, p.429-463, 1 January 2003
	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
	Yoriyuki Yamagata, Strong normalization of the second-order symmetric λμ-calculus, Information and Computation, v.193 n.1, p.1-20, 25 August 2004
	Nobuko Yoshida , Martin Berger , Kohei Honda, Strong normalisation in the π-calculus, Information and Computation, v.191 n.2, p.145-202, 15 June 2004
	Luca Paolini, A stable programming language, Information and Computation, v.204 n.3, p.339-375, March 2006
	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
	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
	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
	Tristan Crolard, A confluent λ-calculus with a catch/throw mechanism, Journal of Functional Programming, v.9 n.6, p.625-647, November 1999
	Hugo Herbelin , Silvia Ghilezan, An approach to call-by-name delimited continuations, ACM SIGPLAN Notices, v.43 n.1, January 2008
	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
	Jason Reed , Frank Pfenning, Intuitionistic Letcc via Labelled Deduction, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.91-111, March, 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