A syntactic theory of sequential control

DOI10.1016/0304-3975(87)90109-5zbMATH Open0643.03011OpenAlexW2054299141MaRDI QIDQ1101435FDOQ1101435

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

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

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)

Cites Work

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

Cited In (47)

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

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)