Classical logic, continuation semantics and abstract machines
From MaRDI portal
Publication:4240152
DOI10.1017/S0956796898003141zbMath0928.68074WikidataQ128126958 ScholiaQ128126958MaRDI QIDQ4240152
Bernhard Reus, Thomas Streicher
Publication date: 3 May 1999
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items
Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ Limiting partial combinatory algebras ⋮ The differential \(\lambda \mu\)-calculus ⋮ Continuation Models for the Lambda Calculus With Constructors ⋮ Unnamed Item ⋮ Call-by-push-value: Decomposing call-by-value and call-by-name ⋮ Negative translations not intuitionistically equivalent to the usual ones ⋮ Adding Negation to Lambda Mu ⋮ Unnamed Item ⋮ Domain-Freeλµ-Calculus ⋮ The next 700 Krivine machines ⋮ On the correctness of the Krivine machine ⋮ A proof-theoretic foundation of abortive continuations ⋮ A Filter Model for the λμ-Calculus ⋮ Classical realizability in the CPS target language ⋮ Krivine's classical realisability from a categorical perspective ⋮ Infinite trace equivalence ⋮ On the unity of duality ⋮ Game semantics and linear CPS interpretation ⋮ A functional interpretation for nonstandard arithmetic ⋮ Completeness of continuation models for \(\lambda_\mu\)-calculus ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Classical By-Need ⋮ Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus ⋮ A Third-Order Representation of the λμ-Calculus ⋮ Adjunction Models For Call-By-Push-Value With Stacks ⋮ CPS-translation as adjoint ⋮ An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. ⋮ Relational Parametricity for Control Considered as a Computational Effect ⋮ The approximation theorem for the Λμ-calculus
