A syntactic theory of sequential control
From MaRDI portal
Publication:1101435
DOI10.1016/0304-3975(87)90109-5zbMath0643.03011OpenAlexW2054299141MaRDI QIDQ1101435
Daniel P. Friedman, Matthias Felleisen, 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
denotational semanticslambda-calculuscontrol operatorsfunctional programsreduction machineChurch-Rosser propertycompiler optimizations
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)
Related Items
A constructive logic behind the catch and throw mechanism, From global to local state, coalgebraically and compositionally, Towards Erlang Verification by Term Rewriting, Programming and Proving with Classical Types, Decomposing typed lambda calculus into a couple of categorical programming languages, A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc, Representing Control: a Study of the CPS Transformation, Unnamed Item, From operational to denotational semantics, Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus, Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\), Sound and complete axiomatisations of call-by-value control operators, Proving the correctness of recursion-based automatic program transformations, Selective strictness and parametricity in structural operational semantics, inequationally, Classical Call-by-Need and Duality, The revised report on the syntactic theories of sequential control and state, A theory for program and data type specification, Musings around the geometry of interaction, and coherence, Programs from proofs using classical dependent choice, A type-theoretic foundation of delimited continuations, A monadic framework for delimited continuations, Unnamed Item, Universe Types for Topology and Encapsulation, Completeness of continuation models for \(\lambda_\mu\)-calculus, Refined program extraction from classical proofs, A Context-based Approach to Proving Termination of Evaluation, Proving the correctness of recursion-based automatic program transformations, A syntactic theory of sequential state, Unnamed Item, Programs with continuations and linear logic, On the unification of classical, intuitionistic and affine logics, A Third-Order Representation of the λμ-Calculus, Model Checking Erlang Programs – Abstracting Recursive Function Calls, Representing Control: a Study of the CPS Transformation, Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus, Delimited control and computational effects
Cites Work
- Unnamed Item
- Unnamed Item
- The lambda calculus, its syntax and semantics
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Scheme: A interpreter for extended lambda calculus
- Continuations: A mathematical semantics for handling full jumps
- Embedding continuations in procedural objects
- A network of microprocessors to execute reduction languages, part II
- Continuation-Based Program Transformation Strategies
- Logic continuations
- GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept
- Proving algorithms by tail functions
- The Mechanical Evaluation of Expressions
