A tool for constructing structures generated by higher-order recursion schemes and collapsible pushdown automata. It is also a pedagogic tool for teaching Game semantics and the theory of traversals (cf. my DPhil thesis).
A termination analysis tool for a Core ML subset based on size-change termination. This tool was developped as part of my Master project on Termination analysis of lambda calculus and a subset of core ML. See the dissertation thesis for explanations on how to use the tool.