The program consists of a series of 32 lectures including foundational theory, advanced techiniques and practical applications. The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions. The lectures start at 9:00 am and go until 5:00 pm with a 2 hour break for lunch and a 15 minute break between sessions.

schedule

	Morning		Afternoon
	Session 1	Session 2	Session 1	Session 2
TUE 7/22	Intro	Harper	Manolios	Weirich
WED 7/23	Weirich	Manolios	Harper	Manolios
THR 7/24	Urban	Harper	Weirich	Sheard
FRI 7/25	Weirich	Sheard	Urban	Panel I
SAT 7/26	Sheard	Urban
MON 7/28	Leino	deMoura	Hickey	Lerner
TUE 7/29	Hickey	Lerner	Leino	deMoura
WED 7/30	deMoura	Lerner	Hickey	Panel II

Leonardo de Moura	SMT Solvers - Theory, Implementation and Applications
Robert Harper Dan Licata	Mechanization of Metatheory Using lf and twelf
Jason Hickey	Compiler Construction in Formal Logical Frameworks
Rustan Leino	Specification and Verification of Programs with Pointers
Sorin Lerner	Leveraging Domain-Specific Languages for Reasoning
Pete Manolios	Reasoning About Programs with ACL2
Tim Sheard	Putting the Curry-Howard Isomorphism to Work
Christian Urban	Nominal Techniques
Stephanie Weirich Brian Aydemir	Coq for Programming Language Metatheory
Panel I
Panel II	Scaling to Significant Systems

Map of the area

This page is the property of the University of Oregon