TALK KEYWORD INDEX

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

A | |

Agda | |

Agda formalisation | |

algebra of programming | |

arithmetic coding | |

B | |

blockchain | |

Breadth-first algorithms | |

C | |

canonicity | |

Compilation | |

completeness | |

confidentiality | |

Coq | |

correctness by extraction | |

Cylindric algebras | |

D | |

delay monad | |

depth-first search | |

derivatives | |

E | |

effects | |

equational reasoning | |

F | |

finite automata | |

Fixpoints | |

folds and unfolds | |

formalisation | |

Frames | |

function extensionality | |

functional programming | |

fusion | |

G | |

Galois connections | |

graph search | |

H | |

Haskell | |

I | |

iteration | |

K | |

Kleene algebra | |

Kleene lattices | |

M | |

metatheory | |

monad | |

monads | |

N | |

non-determinism | |

nondeterminism | |

P | |

parametricity | |

probabilistic program semantics | |

program calculation | |

program derivation | |

program slicing | |

proof irrelevance | |

Q | |

Quantitative Information Flow | |

queues in functional programming | |

R | |

recursive types | |

refinement | |

Refinement calculus | |

regular algebra | |

regular algebras | |

regular expressions | |

relation algebra | |

Relational models | |

reversible computation | |

S | |

Salomaa | |

security | |

set model | |

shallow embedding | |

Smart contracts | |

SSReflect | |

standard model | |

state | |

subfactors | |

synchronous Kleene algebra | |

System F | |

T | |

type systems | |

type theory | |

U | |

univalence | |

V | |

verified implementation |