Monday, 5pm — CSE 407

Subscribe to the calendar: iCal or Google Calendar.

We meet once a month to discuss the practice of proof assistants. There will be food! Please sign up for the PAUG mailing list.

Date	Who	What
Jan 22	John Leo	Programming in Cubical Type Theory One week late due to MLK day.
Feb 1	–	(No meeting this month)
Mar 19	–	(No meeting this month) (This is during Spring break.)
Apr 16	Talia	Spellcraft 101: Demystifying Supertactics
May 21	Calvin	Cozy details
Jun 18	–	–
Jul 16	–	–
Aug 20	Pavel	Cassius details and interacting with Z3
Sep 17	–	–
Oct 15	–	–
Nov 19	–	–
Dec 17	–	–

Topic Suggestions

• brainstorming session on empirical questions/hypotheses about proof engineering
• Morphoid Type Theory (blog post)
• HaysTac, StructTact, and tactic library engineering (collab with UCSD ProgSys)
• Cooqoon Coq IDE
• SMTCoq and Extending SMTCoq
• Floating-Point Verification using Theorem Proving
• Coinduction
• Hyperkernel
• Mechanising and Verifying the WebAssembly Specification
• Logical relations