Focusing on Binding and Computation

Reference. Focusing on Binding and Computation

Cite

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

BibTeX

bibtex · 1 line

@inproceedings{licata-2008-focusing, title={Focusing on Binding and Computation}, ISSN={1043-6871}, url={http://dx.doi.org/10.1109/lics.2008.48}, DOI={10.1109/lics.2008.48}, booktitle={2008 23rd Annual IEEE Symposium on Logic in Computer Science}, publisher={IEEE}, author={Licata, Daniel R. and Zeilberger, Noam and Harper, Robert}, year={2008}, month=June, pages={241–252} }

hayagriva YAML (typst)

yaml · 15 lines

licata-2008-focusing:
  type: article
  title: Focusing on Binding and Computation
  author:
  - Licata, Daniel R.
  - Zeilberger, Noam
  - Harper, Robert
  date: 2008-06
  page-range: 241-252
  serial-number:
    doi: 10.1109/lics.2008.48
  parent:
    type: proceedings
    title: 2008 23rd Annual IEEE Symposium on Logic in Computer Science
    publisher: IEEE

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

Cited by (1)

Syntax for Free: Representing Syntax with Binding Using Parametricity atkey-2009-syntaxTLCA · 2009

DOI

Cites 42 works (4 here)

With notes (4)

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

DOI

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

PDF · DOI · pldb

System Description: Twelf — A Meta-Logical Framework for Deductive Systems pfenning_schrmann_1999CADE · 1999

DOI

Abstract syntax and variable binding fiore_etal_ndLICS

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

DOI

External (38)

Practical Programming with Higher-Order Encodings and Dependent Types (2008)
Contextual modal type theory (2008)
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (2008)
Engineering formal metatheory (2008)
Dependently typed programming with domain-specific logics (draft) (2008)
Focusing on binding and computation (Tech. Rep. CMU-CS-08-101) (2008)
Static Name Control for FreshML (2007)
Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax (2007)
The Coq Proof Assistant Reference Manual (2007)
Towards a practical programming language based on dependent type theory (PhD thesis) (2007)
Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection (2006)
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq (2006)
Consistency of the theory of contexts (2006)
Nominal Techniques in Isabelle/HOL (2005)
FreshML: programming with binders made simple (2003)
a concurrent logical framework i: judgments and properties (2003)
A proof theory for generic judgments: an extended abstract (2003)
Nominal logic, a first order theory of names and binding (2003)
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction (2002)
Locus Solum: From the rules of logic to the logic of rules (2001)
A Metalanguage for Programming with Bound Names Modulo Renaming (2000)
semantical analysis of higher-order (1999)
A new approach to abstract syntax involving binders (1999)
monadic presentations of lambda terms using generalized inductive types (1999)
de Bruijn notation as a nested datatype (1999)
Higher-Order Rewriting with Dependent Types (PhD thesis) (1999)
Primitive recursion for higher-order abstract syntax (1997)
Higher-Order Abstract Syntax in Coq (1995)
Substitution: A Formal Methods Case Study Using Monads and Transformations (1994)
Rules of definitional reflection (1993)
A framework for defining logics (1993)
On the Unity of Logic (1993)
Logic Programming with Focusing Proofs in Linear Logic (1992)
Partial Inductive Definitions (1991)
On computational open-endedness in Martin-Lof's type theory (1991)
an extension to ml to handle bound variables in data structures (1990)
Simple Consequence Relations (1988)
Hauptsatz for the intuitionistic theory of iterated inductive definitions (1971)