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	–	–

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