Classical logic, continuation semantics and abstract machines

DOI10.1017/S0956796898003141zbMATH Open0928.68074WikidataQ128126958 ScholiaQ128126958MaRDI QIDQ4240152FDOQ4240152

Authors: Thomas Streicher, Bernhard Reus 

Publication date: 3 May 1999

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

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

zbMATH Keywords

denotational semanticsabstract machinescontinuation semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Cited In (35)

• An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus.
• Adding Negation to Lambda Mu
• On the correctness of the Krivine machine
• 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
• Frames and topological algebras for a double-power monad
• Call-by-push-value: Decomposing call-by-value and call-by-name
• A functional interpretation for nonstandard arithmetic
• Limiting partial combinatory algebras
• 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
• Title not available (Why is that?)
• 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
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• On the unity of duality
• Game semantics and linear CPS interpretation
• Logic Based Program Synthesis and Transformation
• Title not available (Why is that?)

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)