Sound and complete axiomatisations of call-by-value control operators

DOI10.1017/S0960129500001195zbMath0846.68066OpenAlexW2034257290MaRDI QIDQ4882487

Martin Hofmann

Publication date: 15 July 1996

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500001195

zbMATH Keywords

propositional logiccall-by-value \(\lambda\)-calculus

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) 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 (9)

On the call-by-value CPS transform and its semantics ⋮ Decomposing typed lambda calculus into a couple of categorical programming languages ⋮ Combining algebraic effects with continuations ⋮ Domain-Freeλµ-Calculus ⋮ A proof-theoretic foundation of abortive continuations ⋮ A type-theoretic foundation of delimited continuations ⋮ On the semantics of classical disjunction ⋮ Completeness of continuation models for \(\lambda_\mu\)-calculus ⋮ An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form

Cites Work

• Notions of computation and monads
• A syntactic theory of sequential control
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item

This page was built for publication: Sound and complete axiomatisations of call-by-value control operators