Jasmin Christian Blanchette

Extensions to the Comprehensive Framework for Saturation Theorem Proving
by Jasmin Christian Blanchette and Sophie Tourret

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann

Operations on Bounded Natural Functors
by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Abstract Soundness
by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel

Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Abstract Completeness
by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Sound and Complete Sort Encodings for First-Order Logic
by Jasmin Christian Blanchette and Andrei Popescu

The Textbook Proof of Huffman's Algorithm
by Jasmin Christian Blanchette