Jasmin Christian Blanchette

 

Website: http://www21.in.tum.de/~blanchet

 

Entries

2018

November 23: A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

January 18: Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

 

2017

December 19: Operations on Bounded Natural Functors

February 10: Abstract Soundness

 

2016

November 12: Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

November 12: Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms

September 23: Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

 

2014

April 16: Abstract Completeness

 

2013

June 27: Sound and Complete Sort Encodings for First-Order Logic

 

2008

October 15: The Textbook Proof of Huffman's Algorithm