Posts

• Formalizing finite sets - May 27, 2022
• The pro-PER meaning of "proper" - April 7, 2022
• On proving lists infinite - October 26, 2021
• Initial and final encodings of free monads - October 20, 2021
• hs-to-coq and Data.Sequence - November 23, 2020
• The pl-a.net link aggregators - July 26, 2020
• Free applicative functors in Coq - July 14, 2019
• Formalization of Reynolds's parametricity theorem in Coq - April 3, 2019
• From C to Interaction trees: Specifying, Verifying, and Testing a networked server (CPP 2019 talk transcript) - January 14, 2019