A syntactic theory of sequential control

DOI10.1016/0304-3975(87)90109-5MaRDI QIDQ1101435zbMATH OpenOpenAlexFDO

Authors Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, Bruce Duba

Publication date 1987

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(87)90109-5

zbMATH Keywords

denotational semanticslambda-calculuscontrol operatorsfunctional programsreduction machineChurch-Rosser propertycompiler optimizations

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• A syntactic theory of sequential state
• A complete, co-inductive syntactic theory of sequential control and state
• Publication:4490747
• The revised report on the syntactic theories of sequential control and state
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State

Cites work

• scientific article; zbMATH DE number 3872649 (Why is no real title available?)
• scientific article; zbMATH DE number 3244305 (Why is no real title available?)
• A network of microprocessors to execute reduction languages, part II
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Continuation-Based Program Transformation Strategies
• Continuations: A mathematical semantics for handling full jumps
• Embedding continuations in procedural objects
• GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept
• Logic continuations
• Proving algorithms by tail functions
• Scheme: A interpreter for extended lambda calculus
• The Mechanical Evaluation of Expressions
• The lambda calculus, its syntax and semantics

Cited in

(47)

• A sound and complete bisimulation for contextual equivalence in \(\lambda\)-calculus with call/cc
• Decomposing typed lambda calculus into a couple of categorical programming languages
• Syntactic theories in practice
• A constructive logic behind the catch and throw mechanism
• Programming and Proving with Classical Types
• Towards Erlang verification by term rewriting
• A complete, co-inductive syntactic theory of sequential control and state
• Programs with continuations and linear logic
• Programs from proofs using classical dependent choice
• scientific article; zbMATH DE number 7056232 (Why is no real title available?)
• scientific article; zbMATH DE number 177785 (Why is no real title available?)
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Control reduction theories: the benefit of structural substitution
• Semantics of interference control
• A monadic framework for delimited continuations
• A theory for program and data type specification
• Proving the correctness of recursion-based automatic program transformations
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• Proving the correctness of recursion-based automatic program transformations
• From global to local state, coalgebraically and compositionally
• Universe Types for Topology and Encapsulation
• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• The revised report on the syntactic theories of sequential control and state
• A type-theoretic foundation of delimited continuations
• Representing Control: a Study of the CPS Transformation
• A third-order representation of the \(\lambda\mu\)-calculus
• scientific article; zbMATH DE number 1479632 (Why is no real title available?)
• A context-based approach to proving termination of evaluation
• Representing Control: a Study of the CPS Transformation
• Refined program extraction from classical proofs
• Classical call-by-need and duality
• Relations between Control Mechanisms for Sequential Grammars1
• Selective strictness and parametricity in structural operational semantics, inequationally
• Sound and complete axiomatisations of call-by-value control operators
• scientific article; zbMATH DE number 2064223 (Why is no real title available?)
• Delimited control and computational effects
• Sequential syntactical decoding
• On the unification of classical, intuitionistic and affine logics
• Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
• Musings around the geometry of interaction, and coherence
• Model checking Erlang programs -- abstracting recursive function calls
• Proceedings of the first workshop on control operators and their semantics, COS 2013, Eindhoven, The Netherlands, June 24--25, 2013
• From operational to denotational semantics
• Continuation calculus
• scientific article; zbMATH DE number 7533352 (Why is no real title available?)
• A syntactic theory of sequential state

This page was built for publication: A syntactic theory of sequential control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1101435)