publicações selecionadas A Mechanized Proof of a Textbook Type Unification Algorithm A sound strategy for compiling general recursive functions into finite depth pattern matching The Design of a Verified Derivative-Based Parsing Tool for Regular Expressions
