59:05

SMTCoq: Safe and Efficient Automation in Coq

ACM SIGPLAN

29:00

Verifying Concurrent Go Code in Coq with Goose

ACM SIGPLAN

27:26

An Equations Tutorial

ACM SIGPLAN

25:18

Deriving Instances with Dependent Types

ACM SIGPLAN

56:03

Autosubst 2: Reasoning with de Bruijn Terms and Substitutions

ACM SIGPLAN

29:28

Towards Formally Verified Just-In-Time Compilation

ACM SIGPLAN

30:53

A Coq Library of Undecidable Problems

ACM SIGPLAN

44:08

Session with the Coq Development Team

ACM SIGPLAN