Software

Superposition with datatypes and codatatypes

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