A |

abstract interpretation | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations |

automated induction | HipSpec : Automating Inductive Proofs of Program Properties |

automated theorem proving | HipSpec : Automating Inductive Proofs of Program Properties |

C |

categorical quantum mechanics | Synthesising Graphical Theories |

Conjecture synthesis | Synthesising Graphical Theories |

D |

depth-first search | A Framework for Verified Depth-First Algorithms |

E |

equational reasoning | HipSpec : Automating Inductive Proofs of Program Properties |

F |

floating-point numbers | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations |

G |

graph rewriting | Synthesising Graphical Theories |

I |

Isabelle/HOL | A Framework for Verified Depth-First Algorithms |

M |

machine integers | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations |

model checking | A Framework for Verified Depth-First Algorithms |

model theory | Theory Exploration: a role for Model Theory? |

monoidal categories | Synthesising Graphical Theories |

N |

numeric domains | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations |

P |

program verification | HipSpec : Automating Inductive Proofs of Program Properties |

S |

saturation | Theory Exploration: a role for Model Theory? |

static analysis | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations |

string diagrams | Synthesising Graphical Theories |

T |

testing | HipSpec : Automating Inductive Proofs of Program Properties |

theorem proving | A Framework for Verified Depth-First Algorithms |

theory exploration | Theory Exploration: a role for Model Theory? |

theory formation | HipSpec : Automating Inductive Proofs of Program Properties |