On the unity of duality

DOI10.1016/J.APAL.2008.01.001zbMATH Open1134.03019OpenAlexW2160728467MaRDI QIDQ2482843FDOQ2482843

Authors: Noam Zeilberger 

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

Recommendations

• Elaborating evaluation-order polymorphism
• The duality of classical intersection and union types
• The Duality of Construction
• Call-by-value is dual to call-by-name
• Subtyping and intersection types revisited

zbMATH Keywords

Curry-Howard isomorphismfocusingpolarityevaluation orderMichael Dummett

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites Work

• Untersuchungen über das logische Schliessen. I
• Title not available (Why is that?)
• On the idea of a general proof theory
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A judgmental reconstruction of modal logic
• The Logic of Contradiction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructible falsity
• Linear logic
• Notions of computation and monads
• Computational interpretations of linear logic
• Locus solum: From the rules of logic to the logic of rules.
• Types for Proofs and Programs
• Natural deduction with general elimination rules
• A filter lambda model and the completeness of type assignment
• Title not available (Why is that?)
• Zur Deutung der intuitionistischen Logik
• Control categories and duality: On the categorical semantics of the lambda-mu calculus
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• On the unity of logic
• Classical logic, continuation semantics and abstract machines
• Focussing and proof construction
• The duality of computation
• Classical isomorphisms of types
• On the relations between monadic semantics
• A remark on Gentzen's calculus of sequents
• Title not available (Why is that?)
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Intersection and union types: Syntax and semantics
• A new deconstructive logic: linear logic
• Title not available (Why is that?)
• Intersection types and computational effects
• Call-by-value is dual to call-by-name
• Logical Approaches to Computational Barriers
• Towards a Logic for Pragmatics. Assertions and Conjectures
• Tridirectional typechecking

Cited In (18)

• Many Facets of Dualities
• Structural focalization
• A sequent calculus for a semi-associative law
• Healthiness from Duality
• Classical realizability in the CPS target language
• The polarized \(\lambda\)-calculus
• Cut elimination in multifocused linear logic
• Title not available (Why is that?)
• Polarized subtyping
• Dualized simple type theory
• Delimited control operators prove double-negation shift
• Linear \(\lambda \mu\) is CP (more or less)
• Unilateral Analysis and Duality
• Elaborating evaluation-order polymorphism
• Game of grounds
• Title not available (Why is that?)
• Subtyping and intersection types revisited
• Title not available (Why is that?)

This page was built for publication: On the unity of duality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2482843)