| 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 |
