Call-by-value is dual to call-by-name
From MaRDI portal
Publication:5261275
DOI10.1145/944705.944723zbMath1315.68060OpenAlexW2053198071MaRDI QIDQ5261275
Publication date: 2 July 2015
Published in: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/944705.944723
sequent calculusnatural deductionlogiclambda calculusCurry-Howard correspondencelambda-mu calculusDe Morgan dual
Related Items (26)
Classical Logic with Mendler Induction ⋮ Normalization in the simply typed -calculus ⋮ Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less) ⋮ Categorical proof theory of classical propositional calculus ⋮ Call-by-Value Is Dual to Call-by-Name, Extended ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Classical (co)recursion: Mechanics ⋮ Galois connecting call-by-value and call-by-name ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ 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 ⋮ Unnamed Item ⋮ Investigations on the dual calculus ⋮ Abstracting models of strong normalization for classical calculi ⋮ Unnamed Item ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ Intuitionistic Letcc via Labelled Deduction ⋮ Focalisation and Classical Realisability ⋮ CPS-translation as adjoint ⋮ On the Computational Representation of Classical Logical Connectives
This page was built for publication: Call-by-value is dual to call-by-name
