Classical logic, continuation semantics and abstract machines

DOI10.1017/S0956796898003141MaRDI QIDQ4240152zbMATH OpenWikidataFDO

Authors Thomas Streicher, Bernhard Reus

Publication date 3 May 1999

Published in Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

denotational semanticsabstract machinescontinuation semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 2090723
• On semantics of a term calculus for classical logic
• A proof-theoretic foundation of abortive continuations
• From operational semantics to abstract machines
• An environment machine for the λμ-calculus

Cited in

(35)

• scientific article; zbMATH DE number 2090723 (Why is no real title available?)
• An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus.
• On the correctness of the Krivine machine
• Adding Negation to Lambda Mu
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• The approximation theorem for the \(\Lambda_{\mu}\)-calculus
• A Filter Model for the λμ-Calculus
• CPS-translation as adjoint
• Classical call-by-need sequent calculi: the unity of semantic artifacts
• Classical realizability in the CPS target language
• Call-by-push-value: Decomposing call-by-value and call-by-name
• A functional interpretation for nonstandard arithmetic
• Limiting partial combinatory algebras
• Frames and topological algebras for a double-power monad
• Classical by-need
• The next 700 Krivine machines
• Continuation models for the lambda calculus with constructors
• Relational parametricity for control considered as a computational effect
• Infinite trace equivalence
• The differential \(\lambda \mu\)-calculus
• scientific article; zbMATH DE number 7450001 (Why is no real title available?)
• A proof-theoretic foundation of abortive continuations
• Domain-free \(\lambda\mu\)-calculus
• Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus
• A first-order completeness result about characteristic Boolean algebras in classical realizability
• Adjunction models for call-by-push-value with stacks
• Negative translations not intuitionistically equivalent to the usual ones
• A third-order representation of the \(\lambda\mu\)-calculus
• Classical BI: Its Semantics and Proof Theory
• Krivine's classical realisability from a categorical perspective
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• On the unity of duality
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Game semantics and linear CPS interpretation
• Logic Based Program Synthesis and Transformation

This page was built for publication: Classical logic, continuation semantics and abstract machines

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