Blog (Tag Coq)

2020

• Named goals in Coq

2018

• Proof reuse in Coq using existential variables
• Verifying local definitions in Coq

2017

• Finding bugs in Haskell code by proving it
• Existence and Termination
• Isabelle functions: Always total, sometimes undefined
• How is coinduction the dual of induction?
• Coinduction in Coq and Isabelle