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

Article

Free access

A formulae-as-type notion of control

Author:

Timothy G. GriffinAuthors Info & Claims

POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 47 - 58

https://doi.org/10.1145/96709.96714

Published: 01 December 1989 Publication History

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.

References

[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.

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.

[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. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52(3):205- 237, 1987.

Digital 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.

Digital 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.

[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.

Digital Library

[8]

J. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Volume 7 of Cambridge Tracts in Computer Science, Cambridge University Press, 1989.

Digital Library

[9]

R. }. Hindley and .1. Seldin. Introduction to Combinators and A-Calculus. London Mathematical Society Student Tezts, Cambridge University Press, 1986.

Digital 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.

[11]

P. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4), 1964.

[12]

P. Landin. The next 700 prograrnmmg languages. Commun. ACM, 9(3):157-166, 1966.

Digital 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.

Digital Library

[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 and W. Clinger. The revised3 report on the algorithmic language scheme. SIGPLAN Notices, 21( 12):37-79, 1986.

Digital Library

[17]

G. L. Steele. Common Lisp: The Language. Digital Press, Bedford, MA, 1984.

Digital Library

[18]

S. Stenlund. Combinators, Lambda-Terms and Proof Theory. D. Reidel, Dordrecht, Holland, 1972.

Cited By

Tian MDi YZhang CDeng S(2024)Genesis of the Early Indosinian Darongshan Granitoid in South China: Response to the Subduction of the Eastern Paleo-Tethys OceanGeofluids10.1155/2024/23871802024(1-18)Online publication date: 25-Jan-2024
https://doi.org/10.1155/2024/2387180
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674639
Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Show More Cited By

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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

December 1989

401 pages

ISBN:0897913434

DOI:10.1145/96709

Chairman:
Frances E. Allen

Copyright © 1989 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 1989

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

351
Total Citations
View Citations
1,599
Total Downloads

Downloads (Last 12 months)246
Downloads (Last 6 weeks)20

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tian MDi YZhang CDeng S(2024)Genesis of the Early Indosinian Darongshan Granitoid in South China: Response to the Subduction of the Eastern Paleo-Tethys OceanGeofluids10.1155/2024/23871802024(1-18)Online publication date: 25-Jan-2024
https://doi.org/10.1155/2024/2387180
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674639
Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Mell SBastani OZdancewic S(2023)Ideograph: A Language for Expressing and Manipulating Structured DataElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.377.4377(65-84)Online publication date: 1-Apr-2023
https://doi.org/10.4204/EPTCS.377.4
Fukuda Y(2023)An S4 extension of the λμμ-calculusJournal of Information Processing10.2197/ipsjjip.31.43231(432-439)Online publication date: 2023
https://doi.org/10.2197/ipsjjip.31.432
Accattoli BStorm THirschfeld R(2023)Sharing a Perspective on the 𝜆-CalculusProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622884(179-190)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622884
Müller MSchuster PBrachthäuser JOstermann K(2023)Back to Direct Style: Typed and TightProceedings of the ACM on Programming Languages10.1145/35860567:OOPSLA1(848-875)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586056
Moriconi E(2023)From Proof-Objects to GroundsPerspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction10.1007/978-3-031-51406-7_6(115-138)Online publication date: 13-Dec-2023
https://doi.org/10.1007/978-3-031-51406-7_6
Curien P(2023)Semantics and Syntax, Between Computer Science and MathematicsThe French School of Programming10.1007/978-3-031-34518-0_7(147-174)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_7
Nantes DOlarte CVentura D(2022)A Subexponential View of Domains in Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.357.7357(93-111)Online publication date: 7-Apr-2022
https://doi.org/10.4204/EPTCS.357.7
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents