Tools

An inference rule for the acyclicity property of term algebras

Coming to terms with quantified reasoning

Reasoning about loops using Vampire in KeY

Catamorphism generation and fusion using Coq