TALK KEYWORD INDEX

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

A | |

abstract datatypes | |

algebraic data types | |

amortised resource analysis | |

Automata | |

automation | |

axiomatic semantics | |

B | |

bisimulation | |

branching VASS | |

C | |

certification | |

Church-Rosser | |

coalgebras | |

codata | |

coinduction | |

combinatorics | |

completion | |

complexity | |

complexity analysis | |

complexity of rewriting | |

compression | |

concurrency | |

conditional rewriting | |

Conditional Term Rewriting | |

confluence | |

conservative extension | |

Constraints | |

constructive mathematics | |

context-sensitive rewriting | |

contextual equivalence | |

copattern matching | |

countable choice | |

critical pairs | |

Cycle rewriting | |

D | |

decreasing diagrams | |

deduction modulo | |

dependent elimination | |

dependent types | |

Derivational complexity | |

E | |

Emptiness | |

equivalence | |

exact real-number computation | |

extensional model | |

F | |

Finiteness | |

first-order term rewriting | |

focusing proofs | |

G | |

Geometry of Interaction | |

Graded theories | |

grammars | |

graph rewriting | |

Guarded recursion | |

H | |

hashing | |

higher-order term rewriting | |

I | |

Implicit Complexity | |

implicit computational complexity | |

inductive definitions | |

infinitary lambda-calculus | |

infinitary rewriting | |

Intersection and union types | |

L | |

lambda calculus | |

Lambda encodings | |

lambda-mu calculus | |

Lawvere theories | |

linear logic | |

Logarithmic Space | |

M | |

model checking | |

modularity | |

Monads with arities | |

N | |

near semi-rings | |

Non-linear | |

Non-orthogonality | |

nondeterminism | |

O | |

operational semantics | |

P | |

Pattern matching | |

permutation equivalence | |

Persistency | |

Pointer Machines | |

polynomial interpretations | |

predicate abstraction | |

predicativity | |

Presheaf semantics | |

program equivalence | |

program verification | |

proof construction | |

proof nets | |

proof nets retraction | |

proof search | |

proof terms | |

proof theory | |

Pure Type Systems | |

R | |

Reachability problem | |

relevance logic | |

resolution and superposition | |

Rewriting | |

rewriting logic | |

Rule-Labelling | |

S | |

SAT | |

semantics | |

sequent calculus | |

step-indexing | |

string rewriting | |

Strong normalisation | |

strong normalization | |

subtyping | |

System description | |

System T | |

T | |

term rewriting | |

Term rewriting system | |

Term Rewriting Systems | |

termination | |

termination analysis | |

the B I monoid | |

The dependency pair framework | |

the game of Alonzo | |

theorem proving | |

transfinite reduction | |

Tree-Automata | |

type theory | |

typed lambda-calculus | |

types | |

U | |

Unification | |

usable rules | |

W | |

weak normalization | |

while-programs |