Article

Free access

A calculus for assignments in higher-order languages

Authors:

Mattias Felleisen,

D. P. FriedmanAuthors Info & Claims

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

Page 314

https://doi.org/10.1145/41625.41654

Published: 01 October 1987 Publication History

PDF eReader

Abstract

Imperative assignments are abstractions of recurring programming patterns in purely functional programming languages. When added to higher-order functional languages, they provide a higher-level of modularity and security but invalidate the simple substitution semantics. We show that, given an operational interpretation of a denotational semantics for such a language, it is possible to design a two-level extension of the λ_u-calculus. This calculus provides a location-free rewriting semantics of the language and offers new possibilities for reasoning with assignments. The upper level of the calculus factors out all the steps in a reduction sequence which must be in a linear order; the lower level allows a partial ordering of reduction steps.

References

[1]

ABDALI, S.K., D.S. Wtsz. Storeless semmatics for ALGOL-style block structure, Proe. Conj. Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Springer-Verlag, New York, 1985, to appear.

Digital Library

Google Scholar

[2]

BARENDREGT, H.P. The Lambda Calculus: Its Syntaz and Semantics, North-Holland, Amsterdam, 1981.

Google Scholar

[3]

B ROOKES, S.D. A fully abstract semantics and a proof system for an Algol-like language with sharing, Proc. Conf. Mathematical Foundations o} Programming Semantics, Lecture Notes in Computer Science, Spfinger-Verlag, New York, 1985, to appear.

Digital Library

Google Scholar

[4]

DZ BRUIJN. N.G. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with applications to the Church-Rosser theorem, Indagationes Mathematics 37, 1972, 381- 392.

Crossref

Google Scholar

[5]

DONAHUZ, J.E. Locations considered unnecessary, Acta Inlormatiea 8, 1977, 221-242.

Google Scholar

[6]

FZLLEISEN, S., D.P. FRIEDMAN. Control operators, the SECD-machine, and the A-calculus, Formal Description of Programming Concepts III, North- Holland, Amsterdam, 1986, to appear.

Google Scholar

[7]

HALPERN, J.Y., A.R. MEYER, B.A. TRAKHTEN- BROT. The semantics of local storage, or What makes the free-list free?, Proc. llth ACM Syrup. Principles o{ Programming Languages, 1984, 245-257.

Digital Library

Google Scholar

[8]

LANVIN, P .J. A correspondence between ALGOL 60 and Church's lambda notation, Comm. ACM, 8(2), 1965, 89-101; 158-165.

Digital Library

Google Scholar

[9]

MASON, I. A. Equivalences of first-order Lisp programs, Proc. First S!tmp. Logic in Computer Science, 1986, 105-117.

Google Scholar

[10]

MORRIS, J.H. Protection in programming languages, Comm. A CM 16(8), 1973, 15-21.

Digital Library

Google Scholar

[11]

PLOTKIN, G .D. A structural approach to operational semantics, Tech. Rpt. DAIMI FN-19, Aarhus University, Computer Science Department, 1981.

Google Scholar

[12]

PLOTKIN, G. D. Call-by-name, call-by-value, and the A-calculus, Theoretical Computer Science 1, 1975, 125-159.

Crossref

Google Scholar

Cited By

View all

Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Lee ELhoták O(2023)Simple Reference Immutability for System F<:Proceedings of the ACM on Programming Languages10.1145/36228287:OOPSLA2(857-881)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622828
Kanabar HVivien SAbrahamsson OMyreen MNorrish MPohjola JZanetti R(2023)PureCake: A Verified Compiler for a Lazy Functional LanguageProceedings of the ACM on Programming Languages10.1145/35912597:PLDI(952-976)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591259
Show More Cited By

Recommendations

Definitional interpreters for higher-order programming languages
ACM '72: Proceedings of the ACM annual conference - Volume 2

Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language ...
Definitional Interpreters for Higher-Order Programming Languages

Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming language based on the lambda calculus (i.e., an applicative language ...
Higher-order logic programming languages with constraints: a semantics
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applications

A Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church's Theory of Types and a generic constraint formalism.

Our syntactic formal system, hoHH(C) (higher-order hereditary Harrop formulas with ...

Comments

Information & Contributors

Information

Published In

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

October 1987

326 pages

ISBN:0897912152

DOI:10.1145/41625

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 October 1987

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL87

Sponsor:

SIGPLAN

POPL87: Fourteenth Annual ACM SIGACT-SIGPLAN Symposium on Prnciples of Programming Languages

January 21 - 23, 1987

Munich, West Germany

Acceptance Rates

POPL '87 Paper Acceptance Rate 29 of 108 submissions, 27%;

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

44
Total Citations
View Citations
508
Total Downloads

Downloads (Last 12 months)50
Downloads (Last 6 weeks)13

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Lee ELhoták O(2023)Simple Reference Immutability for System F<:Proceedings of the ACM on Programming Languages10.1145/36228287:OOPSLA2(857-881)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622828
Kanabar HVivien SAbrahamsson OMyreen MNorrish MPohjola JZanetti R(2023)PureCake: A Verified Compiler for a Lazy Functional LanguageProceedings of the ACM on Programming Languages10.1145/35912597:PLDI(952-976)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591259
Vandenbogaerde BStievenart QDe Roover C(2022)Summary-Based Compositional Analysis for Soft Contract Verification2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM55253.2022.00028(186-196)Online publication date: Oct-2022
https://doi.org/10.1109/SCAM55253.2022.00028
Kabir ILi YLhoták O(2020)ιDOT: a DOT calculus with object initializationProceedings of the ACM on Programming Languages10.1145/34282764:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428276
Near JDarais DAbuah CStevens TGaddamadugu PWang LSomani NZhang MSharma NShan ASong D(2019)Duet: an expressive higher-order language and linear type system for statically enforcing differential privacyProceedings of the ACM on Programming Languages10.1145/33605983:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360598
Wang SCao QMohan AHobor A(2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360597
Zuriel YFriedman MSheffi GCohen NPetrank E(2019)Efficient lock-free durable setsProceedings of the ACM on Programming Languages10.1145/33605543:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360554
Henriksen IBilardi GPingali K(2019)Derivative grammars: a symbolic approach to parsing with derivativesProceedings of the ACM on Programming Languages10.1145/33605533:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360553
Wei GChen YRompf T(2019)Staged abstract interpreters: fast and modular whole-program analysis via meta-programmingProceedings of the ACM on Programming Languages10.1145/33605523:OOPSLA(1-32)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360552
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

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

Cited By

Index Terms

Recommendations

Definitional interpreters for higher-order programming languages

Definitional Interpreters for Higher-Order Programming Languages

Higher-order logic programming languages with constraints: a semantics

Comments

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Other Metrics

Article Metrics

Other Metrics

Cited By

PDF

eReader

Login options

Full Access

Abstract

References

Cited By

Index Terms

Recommendations

Definitional interpreters for higher-order programming languages

Definitional Interpreters for Higher-Order Programming Languages

Higher-order logic programming languages with constraints: a semantics

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations