Focusing and higher-order abstract syntax

Reference. Focusing and higher-order abstract syntax

Cite

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

BibTeX

bibtex · 1 line

@inproceedings{zeilberger-2008-focusing, series={POPL08}, title={Focusing and higher-order abstract syntax}, url={http://dx.doi.org/10.1145/1328438.1328482}, DOI={10.1145/1328438.1328482}, booktitle={Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, publisher={ACM}, author={Zeilberger, Noam}, year={2008}, month=Jan, pages={359–369}, collection={POPL08} }

hayagriva YAML (typst)

yaml · 16 lines

zeilberger-2008-focusing:
  type: article
  title: Focusing and higher-order abstract syntax
  author: Zeilberger, Noam
  date: 2008-01
  page-range: 359-369
  url: http://dx.doi.org/10.1145/1328438.1328482
  serial-number:
    doi: 10.1145/1328438.1328482
  parent:
    type: proceedings
    title: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    publisher: ACM
    parent:
      type: proceedings
      title: POPL08

Download: zeilberger-2008-focusing.bib · zeilberger-2008-focusing.yml

Cited by (3)

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory sterling_20212021

The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.

DOI

Polarity and the Logic of Delimited Continuations zeilberger-2010-polarityLICS · 2010

DOI

Focusing on Binding and Computation licata-2008-focusingLICS · 2008

DOI

Cites 40 works (3 here)

With notes (3)

On the unity of duality zeilberger-2008-onAPAL · 2008

DOI

A judgmental reconstruction of modal logic pfenning-2001-aMSCS · 2001

DOI

Higher-order abstract syntax pfenning-1988-higherPLDI · 1988

PDF · DOI · pldb

External (37)

Contextual modal type theory (2008)
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (2008)
Focusing and polarization in intuitionistic logic (2007)
The Twelf Project (software) (2007)
LJQ: A Strongly Focused Calculus for Intuitionistic Logic (2006)
The Coq Proof Assistant Reference Manual Version 8.1 (2006)
Classical isomorphisms of types (2005)
Pattern matching as cut elimination (2004)
Call-by-value is dual to call-by-name (2003)
Etude de la polarisation en logique (2002)
Locus Solum: From the rules of logic to the logic of rules (2001)
Primitive recursion for higher-order abstract syntax (2001)
Control categories and duality: on the categorical semantics of the lambda-mu calculus (2001)
Focussing and proof construction (2001)
The duality of computation (2000)
Coinductive axiomatization of recursive type equality and subtyping (1998)
Proof search issues in some non-classical logics (1998)
On the meanings of the logical constants and the justifications of the logical laws (1996)
Basic Proof Theory (1996)
Higher-order abstract syntax in Coq (1995)
A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure (1995)
The essence of compiling with continuations (1993)
A taste of linear logic (1993)
On the unity of logic (1993)
Logic Programming with Focusing Proofs in Linear Logic (1992)
Pattern matching with dependent types (1992)
Explicit substitutions (1991)
The Logical Basis of Metaphysics (1991)
Notions of computation and monads (1991)
Inductively defined types (1989)
The calculus of constructions (1988)
Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies (1981)
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)
Definitional interpreters for higher-order programming languages (1972)
Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions (1971)
Introduction to Metamathematics (1952)
Untersuchungen über das logische Schließen. I (1935)