A syntactic theory of sequential control
type: Item
instance of: scholarly article
title: A syntactic theory of sequential control
zbMATH Open document ID: 0643.03011
DOI: 10.1016/0304-3975(87)90109-5
author: Matthias Felleisen
author: Daniel P. Friedman
author: Eugene Kohlbecker
author: Bruce Duba
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
review text: The paper presents an exposition of a theory of syntactic control in a lambda-calculus based programming language. First deficiencies of the lambda-calculus as a programming language are discussed and relevant literature reviewed. Although the control problem can be solved in a general setting using continuations, the authors seek to enrich the lambda-calculus by control operators rather than to model these operators within the standard calculus, and to provide a syntactic theory for these operators. The language \(\Lambda_ c\) contains two control operators, one of them giving its argument complete control over the current continuation, and the other representing on abort operation terminating the program and yielding the value of its argument. Operational semantics for the language is defined, and programming in this language is compared with programming in the traditional lambda- calculus. For the new calculus, notions of reduction and computation are defined, and their fundamental properties are proved. It is shown that the extended calculus satisfies the diamond property and contains a Church-Rosser subcalculus (i.e. the interpretation of control operators is to a certain degree independent of a specific evaluation strategy). A standardization theorem is proved and the correctness of the calculus is demonstrated by showing its correspondence with the original machine semantics. As far as reasoning with the calculus is concerned, its soundness is proved, but it is shown that the calculus is incomplete.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 4047684
zbMATH Keywords: functional programs
zbMATH Keywords: Church-Rosser property
zbMATH Keywords: denotational semantics
zbMATH Keywords: reduction machine
zbMATH Keywords: compiler optimizations
zbMATH Keywords: lambda-calculus
zbMATH Keywords: control operators
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90109-5
OpenAlex ID: W2054299141
cites work: The lambda calculus, its syntax and semantics
cites work: Q3339256
cites work: Embedding continuations in procedural objects
cites work: Logic continuations
cites work: The Mechanical Evaluation of Expressions
cites work: A network of microprocessors to execute reduction languages, part II
cites work: Proving algorithms by tail functions
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
cites work: GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept
cites work: Q5531462
cites work: Continuations: A mathematical semantics for handling full jumps
cites work: Scheme: A interpreter for extended lambda calculus
cites work: Continuation-Based Program Transformation Strategies
description: scientific article; zbMATH DE number 4047684