The revised report on the syntactic theories of sequential control and state

DOI10.1016/0304-3975(92)90014-7zbMath0764.68094OpenAlexW2151716725WikidataQ56021135 ScholiaQ56021135MaRDI QIDQ1199538

Robert Hieb, Matthias Felleisen

Publication date: 16 January 1993

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

Full work available at URL: https://doi.org/10.1016/0304-3975(92)90014-7

zbMATH Keywords

\(\lambda_ \nu\)-calculusequational reasoning about imperative programming

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (48)

Semantics of value recursion for Monadic Input/Output ⋮ Applicative bisimilarities for call-by-name and call-by-value \(\lambda\mu\)-calculus ⋮ A categorical interpretation of Landin's correspondence principle ⋮ The impact of higher-order state and control effects on local relational reasoning ⋮ Algebra Unifies Operational Calculi ⋮ Assignment Calculus: A Pure Imperative Language ⋮ A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc ⋮ Control effects as a modality ⋮ A Rewriting Logic Approach to Type Inference ⋮ A Complete, Co-inductive Syntactic Theory of Sequential Control and State ⋮ Encoding abstract syntax without fresh names ⋮ A lazy desugaring system for evaluating programs with sugars ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ A first order logic of effects ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ Control reduction theories: the benefit of structural substitution ⋮ Streams of approximations, equivalence of recursive effectful programs ⋮ Adding Negation to Lambda Mu ⋮ Psi-calculi revisited: connectivity and compositionality ⋮ On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation ⋮ Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction ⋮ Safety of Nöcker's strictness analysis ⋮ Operational interpretations of an extension of F_ω with control operators ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A proof-theoretic foundation of abortive continuations ⋮ Inferring the equivalence of functional programs that mutate data ⋮ A theory for program and data type specification ⋮ On generic context lemmas for higher-order calculi with sharing ⋮ Syntactic Type Soundness for the Region Calculus ⋮ Unnamed Item ⋮ A type-theoretic foundation of delimited continuations ⋮ Capsules and Closures ⋮ On the semantics of classical disjunction ⋮ Concurrent Objects à la Carte ⋮ Investigations on the dual calculus ⋮ Unnamed Item ⋮ Refined program extraction from classical proofs ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ An imperative pure calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Unnamed Item ⋮ Abstraction and Model Checking of Core Erlang Programs in Maude ⋮ Delimited control and computational effects ⋮ What is the natural abstraction level of an algorithm?

Uses Software

• ML
• LISP

Cites Work

• A syntactic theory of sequential control
• The lambda calculus, its syntax and semantics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A syntactic theory of sequential state
• The next 700 programming languages
• The Mechanical Evaluation of Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The revised report on the syntactic theories of sequential control and state