TALK KEYWORD INDEX

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

A | |

abstract interpretation | |

Abstract syntax | |

accumulated weight constraints | |

additive monad | |

algebra in type theory | |

algebraic effects | |

Algebraic Geometry | |

algebraic structures | |

algorithmic complexity | |

allegories | |

Alternating Automata | |

applicative bisimulation distance | |

applicative simulation distance | |

applied lambda-calculus | |

arithmetic circuits | |

Asynchronous Games | |

Automata over infinite words | |

automata theory | |

automated complexity analysis | |

axiomatization | |

B | |

Behavioural metrics | |

Benchmarking | |

Beth models | |

bisimulation | |

boolean algebra | |

Boolean-valued models | |

Bounded expansion | |

Böhm trees | |

Büchi Automaton | |

C | |

call by value | |

Categorical Logic | |

Categorical model | |

Categorical models | |

Categorical Quantum Mechanics | |

Categorical semantics | |

category theory | |

Causal Dependency | |

cellular cohomology | |

Choice sequences | |

choiceless polynomial time | |

Circuit complexity | |

circuit satisfiability | |

classical arithmetic | |

classical realizability | |

clocks | |

Coarse computability | |

coherence theorems | |

coinduction | |

coinduction up-to | |

combinators | |

Complementation | |

complete abstract domains | |

complexity dichotomy | |

compositionality | |

Computability | |

Computation Complexity | |

Computation Tree Logic | |

computational complexity | |

computational monads | |

Computational thinking | |

concurrency | |

concurrency and distributed computation | |

Concurrent games | |

Concurrent Process Calculi | |

Concurrent Separation Logic | |

Concurrent strategies | |

conditional value at risk | |

Confusion | |

Conservativity | |

Constraint Satisfaction Problem | |

constraint satisfaction problems | |

constructive mathematics | |

contextuality | |

Correspondence theory | |

counting classes | |

cross-fertilization | |

cubical type theory | |

Curry-Howard | |

cut elimination | |

cyber-physical systems | |

D | |

Data Races | |

Data words | |

database theory | |

Decidability | |

definability | |

definable while programs | |

denotation | |

denotational semantics | |

dependent choice | |

dependent product types | |

Dependent Refinement Types | |

dependent temporal effects | |

dependent type theory | |

dependent types | |

Description logic | |

descriptive complexity | |

determinacy | |

Deterministic Automata | |

Diagrammatic Reasoning | |

Dialectica interpretation | |

differential dynamic logic | |

differential equation axiomatization | |

Differential Equations | |

differential ghosts | |

Differential Linear Logic | |

Digital libraries | |

Diller-Nahm variant | |

display map category | |

Distribution based objectives | |

Double negation | |

Double-pushout rewriting | |

downward closures | |

duality | |

Dynamic Logic | |

Dynamic nets | |

E | |

effectful bisimilarity | |

ellipsoid method | |

energy games | |

enriched category theory | |

equational logic | |

equivalence relations | |

erasure | |

Event structures | |

expected shortfall | |

expressiveness | |

extensive category | |

F | |

feasibility of functionals | |

finite model property | |

finite model theory | |

finite sum types | |

First order transduction | |

First-order list function | |

first-order logic | |

First-order multiplicative linear logic | |

First-order types | |

fixed-point logic | |

fixpoint logic | |

Flow Analysis | |

flows and nowhere-zero flows | |

Focusing | |

Forest Algebra | |

Forest Algebras | |

formal aspects of program analysis | |

formal topology | |

formal verification | |

Frobenius algebra | |

Full abstraction | |

Functional Analysis | |

Functional interpretation | |

functional programming | |

fuzz | |

Fuzzy logic | |

G | |

Game semantics | |

game theory | |

games and logic | |

generalised species | |

geometry of interaction | |

gluing | |

graph isomorphism | |

graph theory | |

Graphical reasoning | |

Guarded Recursion | |

H | |

halting problem | |

Handlers | |

hereditarily definable sets | |

Hierarchy Theorem | |

higher groups | |

higher inductive types | |

higher-order computability | |

higher-order programs | |

homotopy type theory | |

howe's method | |

hybrid logic | |

hybrid systems | |

I | |

impredicative encodings | |

impredicativity | |

inductive types | |

infinite-state systems | |

information flow | |

integer weights | |

intersection types | |

intersections | |

intuitionistic linear logic | |

Intuitionistic logic | |

irrelevance | |

K | |

Kakutani's fixed point theorem | |

L | |

lambda calculi | |

lambda calculus | |

lambda calculus and combinatory logic | |

lambda-calculus | |

laziness | |

Lean proof assistant | |

linear cliquewidth | |

linear logic | |

Linear Temporal Logic | |

linear time hierarchy | |

locale theory | |

logic | |

logic for PTime | |

Logic on Trees | |

Logical Frameworks | |

logical paradoxes | |

logical predicates | |

LOIS | |

Lower Bounds | |

M | |

magic states | |

Markov decision processes | |

Markov processes | |

Martin-L\"{o}f type theory | |

Martin-Löf type theory | |

Matrix semigroups | |

mean-payoff games | |

mechanised theorem proving | |

mechanized reasoning | |

MMSNP | |

modal logic | |

modal mu | |

modalities | |

model checking | |

model theory | |

Model-checking first-order logic | |

model-checking problems | |

modules | |

monad | |

monitoring | |

monoidal categories | |

MSO | |

MSO on omega-Words | |

MSO transduction | |

multi-objective optimization | |

N | |

N player games | |

Nash equilibrium | |

Negative translations | |

Non-Deterministic Automata | |

non-idempotency | |

Non-lawlike computability | |

non-zero sum games | |

nondeterminism | |

Nowhere dense graphs | |

Nuprl proof assistant | |

O | |

observational equivalence | |

omega-languages | |

Omega-regular languages | |

open games | |

Optimal Upper Bound | |

OR causality | |

oracle Turing machines | |

Origin | |

P | |

parameterized AC^0 | |

Parametricity | |

parity games | |

PDL | |

Persistent places | |

Petri nets | |

pi calculus | |

Pi-calculus | |

pointfree topology | |

polymorphism | |

polynomial functor | |

Polynomial functors | |

polynomial-time tractability | |

presheaf semantics | |

Presheaves | |

Prime Numbers | |

Probabilistic computation | |

probabilistic CTL | |

probabilistic finite automata | |

probabilistic lambda-calculus | |

Probabilistic programs | |

probabilistic systems | |

probabilistic verification | |

profunctor | |

Program Analysis | |

program extraction | |

Program invariant | |

program refinement | |

programming language semantics | |

programming languages | |

progress measure | |

proof nets | |

proof-as-program | |

proofs-as-programs | |

Propositional Dynamic Logic | |

PROPs | |

Q | |

quantale relator | |

quantifier rank | |

quantifiers | |

quantitative algebraic reasoning | |

quantum computation | |

quantum computing | |

quantum program | |

query | |

Query Enumeration | |

R | |

Ramsey theory | |

random variables | |

ranking functions | |

Rational synthesis | |

Real-Time | |

Realizability | |

recognizability | |

register machines | |

regular expressions | |

regular languages | |

relational model | |

relational reasoning | |

resource calculus | |

ribbon categories | |

Riesz modal logic | |

S | |

Satisfiability | |

semantics | |

semantics of programming languages | |

semidefinite programming | |

separability | |

separation | |

separation logic | |

sequent calculus | |

Sequential algorithms | |

sequential types | |

sets with atoms | |

smart grid | |

solving equations | |

sound up-to techniques | |

Stability | |

State Complexity | |

state injection | |

State monad | |

stochastic lambda calculus | |

stochastic shortest path | |

Stone space | |

Streaming string transducers | |

Streams | |

string diagrams | |

strong sums | |

structure theory | |

succinct ordered tree coding | |

sums-of-squares | |

Symmetric monoidal categories | |

Synchronous Programming | |

synthesis | |

System Composition | |

system F | |

Systems decomposition | |

T | |

Taylor expansion | |

temporal logic of repeating values | |

Temporal Verification | |

Tensor logic | |

tensorflow | |

tensorial logic | |

termination | |

the MRDP theorem | |

Theory of Computation | |

transducers | |

transduction | |

tree automata | |

tree-depth | |

Trees | |

True Concurrency | |

truncation levels | |

Turing degrees | |

Two player games | |

two-variable logic | |

type system | |

type systems | |

Type theory | |

U | |

unambiguous | |

unary negation fragment | |

unification | |

uniform one-dimensional fragment | |

Uniform quasi-wideness | |

unions | |

univalent foundations | |

universal algebra | |

universes | |

V | |

VC-density | |

VC-dimension | |

vector addition systems with states | |

view | |

W | |

weighted model counting | |

while programs with atoms | |

Wreath Products | |

Z | |

Zariski topology |