Sanjiv Ranchod

dblp:409/2048 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
1since 2021 · last 2025
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 1 · 1 since 2021

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Theoretical computer science
1 paper
Logic in computer science · 80% Combinatorics and discrete mathematics · 20%

Topics — the 5 heaviest of 5, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Logic in computer science › categorical semantics
abstract syntax
0.912025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution · LICS 2025
Logic in computer science
categorical semantics
0.912025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution · LICS 2025
Combinatorics and discrete mathematics › combinatorics on words
substitutions
0.912025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution · LICS 2025
Logic in computer science
type theory
0.912025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution · LICS 2025
Logic in computer science
variable binding
0.912025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution · LICS 2025

Methods — techniques the papers use, named apart from their topics

initial substitution algebras · 0.9generalised structural recursion · 0.9binding-signature endofunctors · 0.9
YearPublicationVenuePosition
2025 Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
abstract
We develop a unified categorical theory of substructural abstract syntax with variable binding and single-variable (capture-avoiding) substitution. This is done for the gamut of context structural rules given by exchange (linear theory) with weakening (affine theory) or with contraction (relevant theory) and with both (cartesian theory). Specifically, in all four scenarios, we uniformly: define abstract syntax with variable binding as free algebras for binding-signature endofunctors over variables; provide finitary algebraic axiomatisations of the laws of substitution; construct single-variable substitution operations by generalised structural recursion; and prove their correctness, establishing their universal abstract character as initial substitution algebras.
Marcelo P. Fiore, Sanjiv Ranchod
LICS2