Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution

Reference. Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution

Cite

Cite as @fiore-2025-substructural (helia, typst) · \cite{fiore-2025-substructural} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{fiore-2025-substructural, title={Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution}, url={http://dx.doi.org/10.1109/lics65433.2025.00022}, DOI={10.1109/lics65433.2025.00022}, booktitle={2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, publisher={IEEE}, author={Fiore, Marcelo and Ranchod, Sanjiv}, year={2025}, month=June, pages={196–208} }

hayagriva YAML (typst)

yaml · 14 lines

fiore-2025-substructural:
  type: article
  title: Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
  author:
  - Fiore, Marcelo P.
  - Ranchod, Sanjiv
  date: 2025-06
  page-range: 196-208
  serial-number:
    doi: 10.1109/lics65433.2025.00022
  parent:
    type: proceedings
    title: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
    publisher: IEEE

Download: fiore-2025-substructural.bib · fiore-2025-substructural.yml

Cites 31 works (2 here)

With notes (2)

Second-Order and Dependently-Sorted Abstract Syntax fiore-2008-secondLICS · 2008

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 (29)

A Finite Algebraic Presentation of Lawvere Theories in the Object-Classifier Topos (2025)
Taut functors and the difference operator (2025)
Substitution, jumps, and algebraic effects (2014)
Lie structure and composition (talk slides, CT 2014) (2014)
Second-order equational logic (2010)
Second-Order Algebraic Theories (2010)
Operads and PROPs (2008)
Towards a mathematical theory of substitution (invited talk slides, CT 2007) (2007)
A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics (2006)
On the structure of substitution (invited talk slides, MFPS) (2006)
On the operads of J.P. May (2005)
Substitution in Non-wellfounded Syntax with Variable Binding (2003)
A Fully Abstract Model for the pi-calculus (Information and Computation) (2002)
Notes on combinatorial functors (2001)
Finite sets and symmetric simplicial sets (2001)
Abstract Syntax and Variable Binding for Linear Binders (2000)
A new approach to abstract syntax involving binders (1999)
Generalised folds for nested datatypes (1999)
Lectures on Semantics: The Initial Algebra and Final Coalgebra Perspectives (1997)
A fully-abstract model for the pi-calculus (LICS 1996) (1996)
Functional programming with bananas, lenses, envelopes and barbed wire (1991)
Programming in Martin-Löf’s type theory: an introduction (1990)
Foncteurs analytiques et espèces de structures (1986)
A universal property of the convolution monoidal structure (1986)
Une théorie combinatoire des séries formelles (1981)
Strong functors and monoidal monads (1972)
On closed categories of functors (1970)
A fixpoint theorem for complete categories (1968)
Categorical algebra (1965)