The duality of computation
From MaRDI portal
Publication:2943375
DOI10.1145/351240.351262zbMath1321.68146OpenAlexW2016326123MaRDI QIDQ2943375
Pierre-Louis Curien, Hugo Herbelin
Publication date: 11 September 2015
Published in: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/351240.351262
Related Items (78)
Models of Linear Logic based on the Schwartz $\varepsilon$-product ⋮ Classical Logic with Mendler Induction ⋮ Normalization in the simply typed -calculus ⋮ Polarized games ⋮ Parametric parameter passing \(\lambda\)-calculus ⋮ Symmetric categorial grammar ⋮ Probabilistic operational semantics for the lambda calculus ⋮ Open Call-by-Value ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less) ⋮ Categorical proof theory of classical propositional calculus ⋮ Declarative representation of proof terms ⋮ Combining algebraic effects with continuations ⋮ Semantic types and approximation for Featherweight Java ⋮ Call-by-Value Is Dual to Call-by-Name, Extended ⋮ Control reduction theories: the benefit of structural substitution ⋮ Justification logic as a foundation for certifying mobile computation ⋮ Classical (co)recursion: Mechanics ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Galois connecting call-by-value and call-by-name ⋮ A framework for substructural type systems ⋮ Classical realizability and arithmetical formulæ ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ Kripke models for classical logic ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Call-by-name extensionality and confluence ⋮ Unnamed Item ⋮ Dualized Simple Type Theory ⋮ Unnamed Item ⋮ Focused linear logic and the \(\lambda\)-calculus ⋮ A Classical Sequent Calculus with Dependent Types ⋮ A formal language for cyclic operads ⋮ Proof nets for classical logic ⋮ Classical Call-by-Need and Duality ⋮ A Filter Model for the λμ-Calculus ⋮ Classical realizability in the CPS target language ⋮ Covert Movement in Logical Grammar ⋮ Proof Terms for Generalized Natural Deduction ⋮ Classical natural deduction for S4 modal logic ⋮ Continuation semantics for the Lambek-Grishin calculus ⋮ Classical \(F_{\omega}\), orthogonality and symmetric candidates ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ On the unity of duality ⋮ A type-theoretic foundation of delimited continuations ⋮ The proof monad ⋮ Unnamed Item ⋮ On the form of witness terms ⋮ Investigations on the dual calculus ⋮ The Logic of Proofs as a Foundation for Certifying Mobile Computation ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Call-By-Push-Value from a Linear Logic Point of View ⋮ Classical By-Need ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Abstracting models of strong normalization for classical calculi ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form ⋮ On the Values of Reducibility Candidates ⋮ A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$ ⋮ A Fresh Look at the λ-Calculus ⋮ Deriving Natural Deduction Rules from Truth Tables ⋮ Monadic Translation of Intuitionistic Sequent Calculus ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION ⋮ Focalisation and Classical Realisability ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Expansion trees with cut ⋮ Focusing and polarization in linear, intuitionistic, and classical logics ⋮ Unnamed Item ⋮ Adjunction Models For Call-By-Push-Value With Stacks ⋮ Quantitative classical realizability ⋮ On the Computational Representation of Classical Logical Connectives ⋮ Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I
This page was built for publication: The duality of computation
