Polarity and the Logic of Delimited Continuations

Reference. Polarity and the Logic of Delimited Continuations

Noam Zeilberger · LICS · 2010 · focusing · DOI

Cite

Cite as @zeilberger-2010-polarity (helia, typst) · \cite{zeilberger-2010-polarity} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{zeilberger-2010-polarity, title={Polarity and the Logic of Delimited Continuations}, url={http://dx.doi.org/10.1109/lics.2010.23}, DOI={10.1109/lics.2010.23}, booktitle={2010 25th Annual IEEE Symposium on Logic in Computer Science}, publisher={IEEE}, author={Zeilberger, Noam}, year={2010}, month=July, pages={219–227} }

hayagriva YAML (typst)

yaml · 12 lines

zeilberger-2010-polarity:
  type: article
  title: Polarity and the Logic of Delimited Continuations
  author: Zeilberger, Noam
  date: 2010-07
  page-range: 219-227
  serial-number:
    doi: 10.1109/lics.2010.23
  parent:
    type: proceedings
    title: 2010 25th Annual IEEE Symposium on Logic in Computer Science
    publisher: IEEE

Download: zeilberger-2010-polarity.bib · zeilberger-2010-polarity.yml

Cites 45 works (3 here)

With notes (3)

Focusing and higher-order abstract syntax zeilberger-2008-focusingPOPL · 2008

PDF · DOI · pldb

Categories for the Working Mathematician maclane_19711971

Web

Normalization by evaluation for typed lambda calculus with coproducts altenkirch_etal_ndLICS

Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as “normalization by evaluation”, and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.

DOI

External (42)

Resource modalities in game semantics (2010)
Monads in action (2010)
Constructive law of excluded middle (2009)
On the logical content of control delimiters (2009)
The logical basis of evaluation order and pattern-matching (PhD thesis) (2009)
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic (2008)
From Axioms to Analytic Rules in Nonclassical Logics (2008)
Focusing and Polarization in Intuitionistic Logic (2007)
Relational Parametricity for Computational Effects (2007)
Call-by-value λ-calculus and LJQ (2007)
A Substructural Type System for Delimited Continuations (2007)
Polymorphic Delimited Continuations (2007)
Combining algebraic effects with continuations (2007)
Reverse engineering machines with the Yoneda lemma (2006)
A Logical Characterization of Forward and Backward Chaining in the Inverse Method (2006)
An Operational Foundation for Delimited Continuations in the CPS Hierarchy (2005)
About translations of classical logic into polarized linear logic (2003)
A concurrent logical framework I: Judgments and properties (2002)
Focussing and proof construction (2001)
Locus Solum: From the rules of logic to the logic of rules (2001)
Control categories and duality: on the categorical semantics of the lambda-mu calculus (2001)
Call-By-Push-Value (PhD thesis) (2001)
Theories of Programming Languages (1998)
Finite notations for infinite terms (1998)
Classical logic, continuation semantics and abstract machines (1998)
Proof search issues in some non-classical logics (PhD thesis) (1998)
A new deconstructive logic: linear logic (1997)
Categorical Structure of Continuation Passing Style (PhD thesis) (1997)
Type-directed partial evaluation (1996)
Controlling Effects (PhD thesis) (1996)
Representing monads (1994)
On the unity of logic (1993)
Logic Programming with Focusing Proofs in Linear Logic (1992)
Notions of computation and monads (1991)
A new constructive logic: classical logic (1991)
Abstracting control (1990)
A functional abstraction of typed contexts (DIKU TR 89/12) (1989)
The theory and practice of first-class prompts (1988)
Classically and intuitionistically provably recursive functions (1978)
Yoneda structures on 2-categories (1978)
Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus (1937)
Sur quelques points de la logique de M. Brouwer (1929)