TALK KEYWORD INDEX

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

A | |

alpha-equivalence | |

Anti-unification | |

automation | |

B | |

B combinator | |

Bimonad | |

Böhm trees | |

C | |

Categorical Quantum Mechanics | |

category theory | |

Coalgebra Modality | |

coherence | |

coinduction | |

Combinatorics | |

combinatory logic | |

completeness | |

completion | |

complexity | |

complexity classes | |

conditional term rewriting | |

confluence | |

constrained rewriting | |

contractibility | |

Coq | |

correctness criteria | |

critical pair | |

cubical sets | |

Cyclic term-graps | |

D | |

decreasing diagrams | |

denotational semantics | |

dependent type theory | |

E | |

Eilenberg-Moore Category | |

Equational theories | |

F | |

fermionic quantum computing | |

fixed point equations | |

functional programming | |

G | |

gradual typing | |

graph algorithms | |

Gray category | |

Guarded Recursion | |

H | |

higher inductive types | |

higher-order recursion schemes | |

higher-order unification | |

homogeneous types | |

homotopy type theory | |

Hopf Monad | |

I | |

implicit complexity | |

Indexed types | |

Inductive Types | |

inductive-inductive types | |

infinitary rewriting | |

innermost conditional narrowing | |

interactive tool | |

internal language | |

intuitionistic linear logic | |

L | |

lambda calculus | |

lambda-calculus | |

Least general generalization | |

Linear Category | |

linear logic | |

logical relations | |

LOGSPACE | |

M | |

mathematical analysis | |

meaningless terms | |

Mixed Distributive Law | |

modalities | |

monoidal categories | |

Monoidal Coalgebra Modality | |

N | |

nominal terms | |

nominal unification | |

normalisation | |

O | |

over-approximation | |

P | |

polygraph | |

prefix-constrained term rewriting | |

program transformation | |

program transformations | |

proof assistants | |

Proof nets | |

proof terms | |

PSPACE | |

Q | |

Quantum Computing | |

quotient inductive types | |

R | |

Recursive types | |

regular tree grammar | |

regularity preservation | |

rewriting | |

S | |

safe schemes | |

simple types | |

Simply typed lambda calculus | |

string diagrams | |

Subtyping | |

Systems of recursion equations | |

T | |

term rewriting | |

Term Rewriting Systems | |

theorem proving | |

tree automata | |

tree automata completion | |

type inhabitation | |

type theory | |

U | |

univalent foundations | |

Universes | |

W | |

weak diamond property | |

Z | |

zw calculus | |

zx calculus |