FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

A
abstract interpretation	Sound up-to techniques and Complete abstract domains
Abstract syntax	Syntax and Semantics for Operations with Scopes
accumulated weight constraints	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
additive monad	Dialectica models of type theory
algebra in type theory	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
algebraic effects	Syntax and Semantics for Operations with Scopes Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Algebraic Geometry	Polynomial Invariants for Affine Programs
algebraic structures	Free Higher Groups in Homotopy Type Theory
algorithmic complexity	A modal mu perspective on solving parity games in quasipolynomial time.
allegories	Allegories: decidability and graph homomorphisms
Alternating Automata	The State Complexity of Alternating Automata
applicative bisimulation distance	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applicative simulation distance	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applied lambda-calculus	Type-two polynomial-time and restricted lookahead.
arithmetic circuits	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Asynchronous Games	An Asynchronous Soundness Theorem for Concurrent Separation Logic
Automata over infinite words	One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
automata theory	The State Complexity of Alternating Automata
automated complexity analysis	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
axiomatization	Allegories: decidability and graph homomorphisms Riesz Modal Logic with Threshold Operators
B
Behavioural metrics	A van Benthem Theorem for Fuzzy Modal Logic
Benchmarking	A Simple and Optimal Complementation Algorithm for Büchi Automata
Beth models	Computability Beyond Church-Turing via Choice Sequences
bisimulation	Quasi-Open Bisimilarity with Mismatch is Intuitionistic
boolean algebra	Classical realizability as a classifier for nondeterminism
Boolean-valued models	Boolean-Valued Semantics for Stochastic Lambda-Calculus
Bounded expansion	Parameterized circuit complexity of model-checking on sparse structures
Böhm trees	Probabilistic Böhm Trees and Probabilistic Separation
Büchi Automaton	A Simple and Optimal Complementation Algorithm for Büchi Automata
C
call by value	Eager Functions as Processes
Categorical Logic	LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic The Syntax and Semantics of Quantitative Type Theory
Categorical model	Syntax and Semantics for Operations with Scopes
Categorical models	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Categorical Quantum Mechanics	Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics Two complete axiomatisations of pure-state qubit quantum computing
Categorical semantics	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams A Logical Account for Linear Partial Differential Equations A General Framework for Relational Parametricity
category theory	Dialectica models of type theory A Generalized Modality for Recursion What's in a game? A theory of game models
Causal Dependency	Causal Computational Complexity of Distributed Processes
cellular cohomology	Cellular Cohomology in Homotopy Type Theory
Choice sequences	Computability Beyond Church-Turing via Choice Sequences
choiceless polynomial time	On computability and tractability for infinite sets
Circuit complexity	Parameterized circuit complexity of model-checking on sparse structures
circuit satisfiability	Satisfiability in multi-valued circuits
classical arithmetic	A sequent calculus with dependent types for classical arithmetic
classical realizability	A sequent calculus with dependent types for classical arithmetic Classical realizability as a classifier for nondeterminism
clocks	Guarded Computational Type Theory
Coarse computability	An answer to the Gamma question
coherence theorems	Ribbon tensorial logic
coinduction	Every λ-Term is Meaningful for the Infinitary Relational Model
coinduction up-to	Sound up-to techniques and Complete abstract domains
combinators	Regular Transducer Expressions for Regular Transformations over infinite words
Complementation	A Simple and Optimal Complementation Algorithm for Büchi Automata
complete abstract domains	Sound up-to techniques and Complete abstract domains
complexity dichotomy	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
compositionality	Compositional game theory
Computability	An answer to the Gamma question
Computation Complexity	Causal Computational Complexity of Distributed Processes
Computation Tree Logic	Automaton-Based Criteria for Membership in CTL
computational complexity	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
computational monads	An algebraic theory of Markov processes
Computational thinking	Sequential Relational Decomposition
concurrency	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
concurrency and distributed computation	Work Analysis with Resource-Aware Session Types
Concurrent games	The concurrent game semantics of Probabilistic PCF
Concurrent Process Calculi	Causal Computational Complexity of Distributed Processes
Concurrent Separation Logic	An Asynchronous Soundness Theorem for Concurrent Separation Logic
Concurrent strategies	What's in a game? A theory of game models
conditional value at risk	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Confusion	Concurrency and Probability: Removing Confusion, Compositionally
Conservativity	Around Classical and Intuitionistic Linear Logics
Constraint Satisfaction Problem	Satisfiability in multi-valued circuits
constraint satisfaction problems	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
constructive mathematics	Computable decision making on the reals and other spaces via partiality and nondeterminism
contextuality	Logical paradoxes in quantum computation
Correspondence theory	A van Benthem Theorem for Fuzzy Modal Logic
counting classes	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
cross-fertilization	Sound up-to techniques and Complete abstract domains
cubical type theory	On Higher Inductive Types in Cubical Type Theory Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Curry-Howard	Classical realizability as a classifier for nondeterminism
cut elimination	Unification nets: canonical proof net quantifiers
cyber-physical systems	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
D
Data Races	An Asynchronous Soundness Theorem for Concurrent Separation Logic
Data words	Logics for Word Transductions with Synthesis Playing with Repetitions in Data Words Using Energy Games
database theory	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Decidability	Allegories: decidability and graph homomorphisms
definability	Definable decompositions for graphs of bounded linear cliquewidth
definable while programs	On computability and tractability for infinite sets
denotation	Every λ-Term is Meaningful for the Infinitary Relational Model
denotational semantics	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types Probabilistic stable functions on discrete cones are power series. Boolean-Valued Semantics for Stochastic Lambda-Calculus
dependent choice	A sequent calculus with dependent types for classical arithmetic
dependent product types	Dialectica models of type theory
Dependent Refinement Types	A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent temporal effects	A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent type theory	Dialectica models of type theory
dependent types	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types A sequent calculus with dependent types for classical arithmetic Guarded Computational Type Theory
Description logic	A van Benthem Theorem for Fuzzy Modal Logic
descriptive complexity	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth A modal mu perspective on solving parity games in quasipolynomial time.
determinacy	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Deterministic Automata	One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Diagrammatic Reasoning	Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Dialectica interpretation	Dialectica models of type theory
differential dynamic logic	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
differential equation axiomatization	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Equations	A Logical Account for Linear Partial Differential Equations
differential ghosts	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Linear Logic	A Logical Account for Linear Partial Differential Equations
Digital libraries	Computability Beyond Church-Turing via Choice Sequences
Diller-Nahm variant	Dialectica models of type theory
display map category	Dialectica models of type theory
Distribution based objectives	Distribution-based objectives for Markov Decision Processes
Double negation	Around Classical and Intuitionistic Linear Logics
Double-pushout rewriting	Rewriting with Frobenius
downward closures	Separability by piecewise testable languages and downward closures beyond subwords
duality	Riesz Modal Logic with Threshold Operators
Dynamic Logic	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Dynamic nets	Concurrency and Probability: Removing Confusion, Compositionally
E
effectful bisimilarity	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
ellipsoid method	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
energy games	Playing with Repetitions in Data Words Using Energy Games
enriched category theory	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
equational logic	An algebraic theory of Markov processes
equivalence relations	Unary negation fragment with equivalence relations has the finite model property
erasure	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Event structures	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types The concurrent game semantics of Probabilistic PCF
expected shortfall	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
expressiveness	A Theory of Register Monitors
extensive category	Dialectica models of type theory
F
feasibility of functionals	Type-two polynomial-time and restricted lookahead.
finite model property	Unary negation fragment with equivalence relations has the finite model property
finite model theory	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
finite sum types	Dialectica models of type theory
First order transduction	Regular and First Order List Functions
First-order list function	Regular and First Order List Functions
first-order logic	Separability by piecewise testable languages and downward closures beyond subwords
First-order multiplicative linear logic	Unification nets: canonical proof net quantifiers
First-order types	On the number of types in sparse graphs
fixed-point logic	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
fixpoint logic	A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Flow Analysis	Causal Computational Complexity of Distributed Processes
flows and nowhere-zero flows	A theory of linear typings as flows on 3-valent graphs
Focusing	Strong Sums in Focused Logic Around Classical and Intuitionistic Linear Logics
Forest Algebra	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Forest Algebras	Wreath Products of Distributive Forest Algebras
formal aspects of program analysis	Work Analysis with Resource-Aware Session Types
formal topology	Computable decision making on the reals and other spaces via partiality and nondeterminism
formal verification	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Frobenius algebra	Rewriting with Frobenius
Full abstraction	Eager Functions as Processes
Functional Analysis	A Logical Account for Linear Partial Differential Equations
Functional interpretation	Dialectica models of type theory A functional interpretation with state
functional programming	A Generalized Modality for Recursion
fuzz	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Fuzzy logic	A van Benthem Theorem for Fuzzy Modal Logic
G
Game semantics	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic The concurrent game semantics of Probabilistic PCF What's in a game? A theory of game models
game theory	Compositional game theory
games and logic	Distribution-based objectives for Markov Decision Processes
generalised species	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
geometry of interaction	The Geometry of Computation-Graph Abstraction
gluing	Dialectica models of type theory
graph isomorphism	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
graph theory	Allegories: decidability and graph homomorphisms A theory of linear typings as flows on 3-valent graphs
Graphical reasoning	Rewriting with Frobenius
Guarded Recursion	Guarded Computational Type Theory A Generalized Modality for Recursion
H
halting problem	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Handlers	Syntax and Semantics for Operations with Scopes
hereditarily definable sets	On computability and tractability for infinite sets
Hierarchy Theorem	The State Complexity of Alternating Automata
higher groups	Higher Groups in Homotopy Type Theory
higher inductive types	On Higher Inductive Types in Cubical Type Theory Impredicative Encodings of (Higher) Inductive Types
higher-order computability	Type-two polynomial-time and restricted lookahead.
higher-order programs	A Fixpoint Logic and Dependent Effects for Temporal Property Verification
homotopy type theory	On Higher Inductive Types in Cubical Type Theory Cellular Cohomology in Homotopy Type Theory Free Higher Groups in Homotopy Type Theory Higher Groups in Homotopy Type Theory Impredicative Encodings of (Higher) Inductive Types
howe's method	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
hybrid logic	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
hybrid systems	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
I
impredicative encodings	Impredicative Encodings of (Higher) Inductive Types
impredicativity	Impredicative Encodings of (Higher) Inductive Types
inductive types	Impredicative Encodings of (Higher) Inductive Types
infinite-state systems	Separability by piecewise testable languages and downward closures beyond subwords
information flow	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
integer weights	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
intersection types	Every λ-Term is Meaningful for the Infinitary Relational Model
intersections	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
intuitionistic linear logic	Around Classical and Intuitionistic Linear Logics
Intuitionistic logic	Quasi-Open Bisimilarity with Mismatch is Intuitionistic
irrelevance	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
K
Kakutani's fixed point theorem	Distribution-based objectives for Markov Decision Processes
L
lambda calculi	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
lambda calculus	Probabilistic stable functions on discrete cones are power series. Eager Functions as Processes
lambda calculus and combinatory logic	A theory of linear typings as flows on 3-valent graphs
lambda-calculus	Every λ-Term is Meaningful for the Infinitary Relational Model
laziness	A sequent calculus with dependent types for classical arithmetic
Lean proof assistant	Higher Groups in Homotopy Type Theory
linear cliquewidth	Definable decompositions for graphs of bounded linear cliquewidth
linear logic	LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic The Syntax and Semantics of Quantitative Type Theory Unification nets: canonical proof net quantifiers Work Analysis with Resource-Aware Session Types Around Classical and Intuitionistic Linear Logics A theory of linear typings as flows on 3-valent graphs
Linear Temporal Logic	One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata Automaton-Based Criteria for Membership in CTL
linear time hierarchy	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
locale theory	Computable decision making on the reals and other spaces via partiality and nondeterminism
logic	Logics for Word Transductions with Synthesis
logic for PTime	On computability and tractability for infinite sets
Logic on Trees	Wreath Products of Distributive Forest Algebras
Logical Frameworks	Strong Sums in Focused Logic
logical paradoxes	Logical paradoxes in quantum computation
logical predicates	Dialectica models of type theory
LOIS	On computability and tractability for infinite sets
Lower Bounds	The State Complexity of Alternating Automata
M
magic states	Logical paradoxes in quantum computation
Markov decision processes	Distribution-based objectives for Markov Decision Processes Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Markov processes	An algebraic theory of Markov processes
Martin-L\"{o}f type theory	Impredicative Encodings of (Higher) Inductive Types
Martin-Löf type theory	Dialectica models of type theory
Matrix semigroups	Polynomial Invariants for Affine Programs
mean-payoff games	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
mechanised theorem proving	Quasi-Open Bisimilarity with Mismatch is Intuitionistic
mechanized reasoning	Cellular Cohomology in Homotopy Type Theory
MMSNP	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
modal logic	A van Benthem Theorem for Fuzzy Modal Logic Quasi-Open Bisimilarity with Mismatch is Intuitionistic
modal mu	A modal mu perspective on solving parity games in quasipolynomial time.
modalities	Guarded Computational Type Theory
model checking	Distribution-based objectives for Markov Decision Processes
model theory	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Model-checking first-order logic	Parameterized circuit complexity of model-checking on sparse structures
model-checking problems	Tree depth, quantifier elimination, and quantifier rank
modules	Strong Sums in Focused Logic
monad	Syntax and Semantics for Operations with Scopes
monitoring	A Theory of Register Monitors
monoidal categories	Compositional game theory Two complete axiomatisations of pure-state qubit quantum computing
MSO	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
MSO on omega-Words	LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic
MSO transduction	Regular and First Order List Functions
multi-objective optimization	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
N
N player games	Rational Synthesis Under Imperfect Information
Nash equilibrium	Rational Synthesis Under Imperfect Information
Negative translations	Around Classical and Intuitionistic Linear Logics
Non-Deterministic Automata	One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
non-idempotency	Every λ-Term is Meaningful for the Infinitary Relational Model
Non-lawlike computability	Computability Beyond Church-Turing via Choice Sequences
non-zero sum games	Rational Synthesis Under Imperfect Information
nondeterminism	Classical realizability as a classifier for nondeterminism
Nowhere dense graphs	On the number of types in sparse graphs
Nuprl proof assistant	Computability Beyond Church-Turing via Choice Sequences
O
observational equivalence	Probabilistic Böhm Trees and Probabilistic Separation
omega-languages	A Theory of Register Monitors
Omega-regular languages	Automaton-Based Criteria for Membership in CTL
open games	Compositional game theory
Optimal Upper Bound	A Simple and Optimal Complementation Algorithm for Büchi Automata
OR causality	Concurrency and Probability: Removing Confusion, Compositionally
oracle Turing machines	Type-two polynomial-time and restricted lookahead.
Origin	Logics for Word Transductions with Synthesis
P
parameterized AC^0	Tree depth, quantifier elimination, and quantifier rank A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Parametricity	A General Framework for Relational Parametricity Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
parity games	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games A modal mu perspective on solving parity games in quasipolynomial time.
PDL	Wreath Products of Distributive Forest Algebras
Persistent places	Concurrency and Probability: Removing Confusion, Compositionally
Petri nets	Concurrency and Probability: Removing Confusion, Compositionally
pi calculus	Eager Functions as Processes
Pi-calculus	Quasi-Open Bisimilarity with Mismatch is Intuitionistic
pointfree topology	Computable decision making on the reals and other spaces via partiality and nondeterminism
polymorphism	Impredicative Encodings of (Higher) Inductive Types
polynomial functor	Dialectica models of type theory
Polynomial functors	What's in a game? A theory of game models
polynomial-time tractability	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
presheaf semantics	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Presheaves	What's in a game? A theory of game models
Prime Numbers	The State Complexity of Alternating Automata
Probabilistic computation	Probabilistic stable functions on discrete cones are power series.
probabilistic CTL	Riesz Modal Logic with Threshold Operators
probabilistic finite automata	Distribution-based objectives for Markov Decision Processes
probabilistic lambda-calculus	Probabilistic Böhm Trees and Probabilistic Separation
Probabilistic programs	The concurrent game semantics of Probabilistic PCF
probabilistic systems	Distribution-based objectives for Markov Decision Processes
probabilistic verification	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
profunctor	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Program Analysis	Polynomial Invariants for Affine Programs
program extraction	A functional interpretation with state
Program invariant	Polynomial Invariants for Affine Programs
program refinement	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
programming language semantics	Computable decision making on the reals and other spaces via partiality and nondeterminism Work Analysis with Resource-Aware Session Types
programming languages	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
progress measure	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
proof nets	Unification nets: canonical proof net quantifiers
proof-as-program	Classical realizability as a classifier for nondeterminism
proofs-as-programs	A sequent calculus with dependent types for classical arithmetic
Propositional Dynamic Logic	Wreath Products of Distributive Forest Algebras
PROPs	Rewriting with Frobenius
Q
quantale relator	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
quantifier rank	Tree depth, quantifier elimination, and quantifier rank
quantifiers	Unification nets: canonical proof net quantifiers
quantitative algebraic reasoning	An algebraic theory of Markov processes
quantum computation	Two complete axiomatisations of pure-state qubit quantum computing Logical paradoxes in quantum computation
quantum computing	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
quantum program	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
query	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Query Enumeration	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
R
Ramsey theory	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
random variables	Boolean-Valued Semantics for Stochastic Lambda-Calculus
ranking functions	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Rational synthesis	Rational Synthesis Under Imperfect Information
Real-Time	A Theory of Register Monitors
Realizability	Classical realizability as a classifier for nondeterminism
recognizability	Definable decompositions for graphs of bounded linear cliquewidth
register machines	A Theory of Register Monitors
regular expressions	Regular Transducer Expressions for Regular Transformations over infinite words
regular languages	Separability by piecewise testable languages and downward closures beyond subwords
relational model	Every λ-Term is Meaningful for the Infinitary Relational Model
relational reasoning	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
resource calculus	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
ribbon categories	Ribbon tensorial logic
Riesz modal logic	Riesz Modal Logic with Threshold Operators
S
Satisfiability	Unary negation fragment with equivalence relations has the finite model property
semantics	Every λ-Term is Meaningful for the Infinitary Relational Model
semantics of programming languages	The Geometry of Computation-Graph Abstraction
semidefinite programming	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
separability	Separability by piecewise testable languages and downward closures beyond subwords
separation	Probabilistic Böhm Trees and Probabilistic Separation
separation logic	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
sequent calculus	A sequent calculus with dependent types for classical arithmetic
Sequential algorithms	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
sequential types	Every λ-Term is Meaningful for the Infinitary Relational Model
sets with atoms	On computability and tractability for infinite sets
smart grid	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
solving equations	Satisfiability in multi-valued circuits
sound up-to techniques	Sound up-to techniques and Complete abstract domains
Stability	On the number of types in sparse graphs
State Complexity	The State Complexity of Alternating Automata
state injection	Logical paradoxes in quantum computation
State monad	A functional interpretation with state
stochastic lambda calculus	Boolean-Valued Semantics for Stochastic Lambda-Calculus
stochastic shortest path	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Stone space	On the number of types in sparse graphs
Streaming string transducers	Regular and First Order List Functions
Streams	A Generalized Modality for Recursion
string diagrams	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams Rewriting with Frobenius Two complete axiomatisations of pure-state qubit quantum computing
strong sums	Strong Sums in Focused Logic
structure theory	Satisfiability in multi-valued circuits
succinct ordered tree coding	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
sums-of-squares	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Symmetric monoidal categories	Rewriting with Frobenius
Synchronous Programming	A Generalized Modality for Recursion
synthesis	Logics for Word Transductions with Synthesis
System Composition	Sequential Relational Decomposition
system F	Impredicative Encodings of (Higher) Inductive Types
Systems decomposition	Sequential Relational Decomposition
T
Taylor expansion	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
temporal logic of repeating values	Playing with Repetitions in Data Words Using Energy Games
Temporal Verification	A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Tensor logic	Around Classical and Intuitionistic Linear Logics
tensorflow	The Geometry of Computation-Graph Abstraction
tensorial logic	Ribbon tensorial logic
termination	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
the MRDP theorem	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Theory of Computation	A General Framework for Relational Parametricity
transducers	Regular Transducer Expressions for Regular Transformations over infinite words
transduction	Logics for Word Transductions with Synthesis Definable decompositions for graphs of bounded linear cliquewidth
tree automata	Automaton-Based Criteria for Membership in CTL
tree-depth	Tree depth, quantifier elimination, and quantifier rank
Trees	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
True Concurrency	An Asynchronous Soundness Theorem for Concurrent Separation Logic
truncation levels	Free Higher Groups in Homotopy Type Theory
Turing degrees	An answer to the Gamma question
Two player games	Playing with Repetitions in Data Words Using Energy Games
two-variable logic	Weighted model counting beyond two-variable logic
type system	Causal Computational Complexity of Distributed Processes
type systems	A Generalized Modality for Recursion Work Analysis with Resource-Aware Session Types A theory of linear typings as flows on 3-valent graphs
Type theory	Computability Beyond Church-Turing via Choice Sequences The Syntax and Semantics of Quantitative Type Theory Guarded Computational Type Theory
U
unambiguous	Regular Transducer Expressions for Regular Transformations over infinite words
unary negation fragment	Unary negation fragment with equivalence relations has the finite model property
unification	Unification nets: canonical proof net quantifiers
uniform one-dimensional fragment	Weighted model counting beyond two-variable logic
Uniform quasi-wideness	On the number of types in sparse graphs
unions	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
univalent foundations	On Higher Inductive Types in Cubical Type Theory
universal algebra	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
universes	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types Guarded Computational Type Theory
V
VC-density	On the number of types in sparse graphs
VC-dimension	On the number of types in sparse graphs
vector addition systems with states	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
view	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
W
weighted model counting	Weighted model counting beyond two-variable logic
while programs with atoms	On computability and tractability for infinite sets
Wreath Products	Wreath Products of Distributive Forest Algebras
Z
Zariski topology	Polynomial Invariants for Affine Programs

Disclaimer | Powered by EasyChair Smart Program