article

Free access

Correspondence between ALGOL 60 and Church's Lambda-notation: part I

Author:

P. J. LandinAuthors Info & Claims

Communications of the ACM, Volume 8, Issue 2

Pages 89 - 101

https://doi.org/10.1145/363744.363749

Published: 01 February 1965 Publication History

PDF eReader

References

[1]

BARRON, D. W., BUXTON, J. N., HARTLEY, D. F., NIXON, E., AND STRACHEY, C. The main features of CPL. Comput, J. 6, 2 (July 1963), 134-143.

Google Scholar

[2]

CURRY, H. B., AND FEYS, R. Combinatory Logic, Vol. 1. North Holland, Amsterdam, 1958.

Google Scholar

[3]

LANDIN, P. J. The mechanical evaluation of expressions. Comput. J. 6, 4 (Jan. 1964), 308-320.

Crossref

Google Scholar

[4]

McCARTHY, J., ET AL. LISP 1.5 Programmer's Manual. MIT, Cambridge, 1962.

Digital Library

Google Scholar

[5]

----. Towards a mathematical science of computation. IFIP Munich Conference 1962. North Holland, Amsterdam, 1963.

Google Scholar

[6]

NAUR, P., ET AL. Revised Report on the Algorithmic Language ALGOL 60. Comm. ACM 6, 1 (Jan. 1963), 1-17.

Digital Library

Google Scholar

[7]

ROSENBLOOM, P. The Elements of Mathematical Logic. Dover, New York, 1950.

Google Scholar

[8]

STRACHEY, C., AND WILKES, M. V. Some proposals for improving the efficiency of ALGOL 60. Comm. ACM 4, 11 (Nov, 1961), 488-491.

Digital Library

Google Scholar

[9]

BOHM, C. The CUCH as a formal and descriptive language. Presented at IFIP Working Conf., Baden, Sept. 1964.

Google Scholar

[10]

LANDIN, P. J. A formal description of ALGOL 60. Presented at IFIP Working Conf., Baden, Sept. 1964.

Google Scholar

[11]

VAN WIJNGAARDEN, A. Recursive definition of syntax and semantics. Presented at IFIP Working Conf., Baden, Sept. 1964.

Google Scholar

[12]

CONWAY, M. E. Design of a separable transition-diagram compiler. Comm. ACM 6, 7 (July 1963), 396-408.

Digital Library

Google Scholar

Cited By

View all

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
Kiselyov O(2024)Generating CScience of Computer Programming10.1016/j.scico.2023.103015231:COnline publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1016/j.scico.2023.103015
Coquand T(2023)Some Remarks About Dependent Type TheoryThe French School of Programming10.1007/978-3-031-34518-0_8(175-202)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_8
Show More Cited By

Index Terms

Correspondence between ALGOL 60 and Church's Lambda-notation: part I

Recommendations

ALGOL 60 confidential

The ALGOL 60 Report,^* when first encountered, seems to describe a very complex language which will be difficult to learn. The “metalinguistic formulae” admirably serve the purpose of precisely specifying a language, but they are certainly not very ...
More Church–Rosser Proofs

The proofs of the Church–Rosser theorems for β, η, and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and ...
Decision tables in Algol 60
Abstract
This paper defines an extension to Algol 60, which allows the programmer to write decision tables in his Algol program. A pre-processor converts the decision tables to Algol, and its output is used as input to the ordinary Algol compiler. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 8, Issue 2

Feb. 1965

71 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/363744

Editor:
C. C. Gotlieb
Univ. of Toronto, Toronto, Ont., Canada

Issue’s Table of Contents

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 February 1965

Published in CACM Volume 8, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

372
Total Citations
View Citations
2,917
Total Downloads

Downloads (Last 12 months)425
Downloads (Last 6 weeks)54

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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
Kiselyov O(2024)Generating CScience of Computer Programming10.1016/j.scico.2023.103015231:COnline publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1016/j.scico.2023.103015
Coquand T(2023)Some Remarks About Dependent Type TheoryThe French School of Programming10.1007/978-3-031-34518-0_8(175-202)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_8
Dybjer PSander H(2022)A functional programming approach to the specification and verification of concurrent systemsFormal Aspects of Computing10.1007/BF018872111:1(303-319)Online publication date: 2-Jan-2022
https://dl.acm.org/doi/10.1007/BF01887211
Cimini MMourad B(2021)Language Transformations in the ClassroomElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.339.6339(43-58)Online publication date: 23-Aug-2021
https://doi.org/10.4204/EPTCS.339.6
Pezlar I(2021)Meaning and Computing: Two Approaches to Computable PropositionsLogic, Language, Information, and Computation10.1007/978-3-030-88853-4_7(100-116)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88853-4_7
Accattoli BDal Lago UVanoni GGabbrielli MAbel ACheney J(2020)The Machinery of InteractionProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414108(1-15)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414108
MacQueen DHarper RReppy J(2020)The history of Standard MLProceedings of the ACM on Programming Languages10.1145/33863364:HOPL(1-100)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3386336
Dewey KHairapetian SGavrilov M(2020)MiMIs: Simple, Efficient, and Fast Bounded-Exhaustive Test Case Generators2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST46399.2020.00016(51-62)Online publication date: Oct-2020
https://doi.org/10.1109/ICST46399.2020.00016
Carvalho FDuarte LGouesse J(2020)Text Web Templates Considered HarmfulWeb Information Systems and Technologies10.1007/978-3-030-61750-9_4(69-95)Online publication date: 3-Nov-2020
https://doi.org/10.1007/978-3-030-61750-9_4
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

References

Cited By

Index Terms

Recommendations

ALGOL 60 confidential

More Church–Rosser Proofs

Decision tables in Algol 60

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations