On the unity of duality

DOI10.1016/J.APAL.2008.01.001MaRDI QIDQ2482843zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(18)

• scientific article; zbMATH DE number 3323293 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7243675 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7204452 (Why is no real title available?)
• Subtyping and intersection types revisited

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)