TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
2 | |
2-categories | |
A | |
Agda | |
algebraic effect | |
Algebraic Hierarchy | |
Anti-unification | |
arithmetic | |
Atomicity | |
automatic analysis | |
Average-case complexity | |
B | |
bar recursion | |
behavioral equivalence | |
Binary fuzzy relations | |
bisimilarity | |
Bunched logic | |
C | |
call-by-value lambda calculus | |
Cartesian difference categories | |
Cartesian differential categories | |
categories of algebras and coalgebras | |
category theory | |
certification | |
Change actions | |
collapse theories | |
complexity | |
Comprehension categories | |
Comprehension structures | |
Comprehension structures with image | |
Comprehension structures with section | |
computational lambda calculus | |
Concurrency | |
Concurrent Kleene Algebra | |
conditional bisimilarity | |
constraint solving | |
Constructive Logic | |
continuation-passing style | |
continuity | |
Coq | |
D | |
D-categories | |
data-flow analysis | |
decidability | |
decision procedure | |
decision trees | |
delimited control | |
Delta-framework | |
dependency pair framework | |
dependent type theory | |
dependent types | |
Difference lambda-calculus | |
Differential lambda-calculus | |
E | |
effect systems | |
Elpi | |
Eta-conversion | |
Extensionality | |
F | |
Frame rules | |
G | |
Game Logic | |
Game Semantics | |
Goedel's System T | |
graded monads | |
graph transformation | |
H | |
handler | |
Higher inductive inductive types | |
higher-order grammar | |
higher-order logic | |
Higher-order model checking | |
Higher-Order Open Programs | |
higher-order recursive path ordering | |
higher-order rewriting | |
higher-order term rewriting | |
HOL | |
Hybrid Games | |
Hybrid semantics | |
I | |
indexing data structures | |
inductive types | |
Intensional type theory | |
Intersection type system | |
Intersection Types | |
Intuitionistic logic | |
Isabelle/HOL | |
K | |
Knuth-Bendix completion | |
L | |
Lambda Calculus | |
Language-integrated query | |
Lawvere categories | |
lens | |
Linear Logic | |
Local reasoning | |
Logical Framework | |
logical relation | |
M | |
majorizability | |
mechanization | |
Metaprogramming | |
Modal Type System | |
model checking problem | |
Modules over monads | |
monadic translation | |
monads | |
mutual inductive types | |
N | |
negative translation | |
Nested relational calculus | |
O | |
Operational semantics | |
optic | |
P | |
Packed Classes | |
pattern matching | |
Pomsets | |
Probabilistic Computation | |
probabilistic logics | |
Profunctors | |
Proof theory | |
Q | |
quotient | |
quotient inductive type | |
Quotient structures | |
R | |
reactive systems | |
reasoning by induction and coinduction | |
reduction order | |
Refinement | |
refinement types | |
refiner | |
reflection | |
resource analysis | |
rewriting | |
S | |
Scott Semantics | |
Semantics | |
semi-unification | |
Separation | |
Sequent calculus | |
session types | |
shallow term rewriting systems | |
similarity relations | |
Solvability | |
Species | |
string diagram | |
Strong normalization | |
subject-reduction | |
subtyping | |
Symbolic Execution | |
systems | |
T | |
Term indexing | |
term rewriting | |
termination | |
termination analysis | |
theorem proving | |
theorem-proving | |
Tree automata | |
tree grammars | |
tree language | |
TT-lifting | |
type checker | |
type systems | |
Type theory | |
type-checking | |
U | |
undecidability | |
unification | |
union types | |
uniqueness of normal forms w.r.t. conversion | |
unital theories | |
Universe polymorphism | |
up-to context | |
Useless analysis | |
V | |
verification | |
W | |
W-types | |
word language | |
Y | |
Yoneda lemma | |
Z | |
Zeno behaviour | |
λ | |
λProlog |