Visible to the public Coq IntensiveConflict Detection Enabled

Submitted by Anonymous on Thu, 01/26/2017 - 2:40pm
Jul 13, 2017 7:00 am - Jul 15, 2017 6:00 pm EDT

Coq Intensive

Overview

The DeepSpec Summer School on Verified Systems summer school will open with a three-day intensive course on the fundamentals of the Coq proof assistant, for participants who are new to Coq. The main lectures take place during the weeks of July 17 and 24.

  • July 13-15 (Thu-Sat) Coq intensive
  • July 17-21 Week 1
  • July 24-28 Week 2

Lecturers and Topics

  • Andrew Appel - Verified functional algorithms
  • Adam Chlipala - Program-specific proof automation
  • Frans Kaashoek & Nickolai Zeldovich - Certifying software with crashes
  • Xavier Leroy - The structure of a verified compiler
  • Benjamin Pierce - Property-based random testing with QuickChick
  • Zhong Shao - CertiKOS: Certified kit operating systems
  • Stephanie Weirich - Language specification and variable binding
  • Steve Zdancewic - Vellvm: Verifying the LLVM

More information

To apply, or for more information, please visit http://deepspec.org/events/ss17detail.html

Applications received by Feb 15 will be given equal consideration; applications received after Feb 15 will be considered on a space- and funds-available basis.