Skip to main content
PRL Project

Related Lectures, Courses, and Discussions

CS6110-Advanced Programming Languages
Course Home Page 2009, 2010, 2011, 2012, 2013, 2014, 2015

CS4860-Applied Logic
Course Home Page 2001, 2003, 2005, 2009, 2010, 2012, 2016

CS5860-Introduction to Formal Methods
Course Home Page 2011, 2014

CS6860-Logics of Programs
Course Home Page 2010

CS6862-Automated Reasoning and Formal Methods
Course Home Page 2011

CS671-Introduction to Automated Reasoning
Course Home Page 2002

Marktoberdorf Summer School
1997, 2001, 2003, 2005, 2007, 2007 slides
The Summer School Marktoberdorf is a two weeks' course for young computer scientists and mathematicians working in the field of "Analysis and Verification of Software Systems"

Oregon Programming Languages Summer School
Lecture Slides and Videos

  • 2015 - look for Robert Constable and Mark Bickford
  • 2012 - look for Proofs as Processes (slides: PDF)
  • 2011 - look for Polymorphic Logic and Design Issues for Implemented Type Theories
  • 2010 - look for Proofs-as-Processes: Reasoning about Concurrency in Computational Type Theory

2011 lectures are presented by internationally recognized leaders in programming languages and formal reasoning research.

Principia Mathematica Anniversary Symposium
Paper: Triumph of Types
This lecture examines the influence of Principia Mathematica on modern type theories implemented in software systems known as interactive proof assistants. These proof assistants advance daily the goal for which Principia was designed: to provide a comprehensive formalization of mathematics.

The Calculemus Autumn School
Slides The Nuprl Proof Development System

Machine Intelligence Research Institute (MIRI)
Interview: Robert Constable on correct-by-construction programming. March 2, 2014.

The Type Theory Podcast
Podcast: Bob Constable on CTT and Nuprl. August 31, 2015.