On the unity of duality
From MaRDI portal
Publication:2482843
DOI10.1016/j.apal.2008.01.001zbMath1134.03019OpenAlexW2160728467MaRDI QIDQ2482843
Publication date: 24 April 2008
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2008.01.001
Theory of programming languages (68N15) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less) ⋮ Structural Focalization ⋮ Unnamed Item ⋮ Delimited control operators prove double-negation shift ⋮ Classical realizability in the CPS target language ⋮ The polarized \(\lambda\)-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Game of grounds ⋮ Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- On the unity of logic
- Computational interpretations of linear logic
- Notions of computation and monads
- On the relations between monadic semantics
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- A remark on Gentzen's calculus of sequents
- On the idea of a general proof theory
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Natural deduction with general elimination rules
- Zur Deutung der intuitionistischen Logik
- Untersuchungen über das logische Schliessen. I
- Focussing and proof construction
- Intersection and union types: Syntax and semantics
- Control categories and duality: on the categorical semantics of the lambda-mu calculus
- Locus Solum: From the rules of logic to the logic of rules
- A judgmental reconstruction of modal logic
- Intersection types and computational effects
- The duality of computation
- A filter lambda model and the completeness of type assignment
- Classical isomorphisms of types
- Tridirectional typechecking
- The Logic of Contradiction
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- Classical logic, continuation semantics and abstract machines
- A new deconstructive logic: linear logic
- Towards a Logic for Pragmatics. Assertions and Conjectures
- Call-by-value is dual to call-by-name
- Types for Proofs and Programs
- Constructible falsity
- Logical Approaches to Computational Barriers
