Theorem Proving in Istari
Course ID 15718
Description The course covers the Istari proof assistant: its type theory and its practical use in proving theorems and reasoning about programs.
Key Topics
Martin-Lof type theories in general, the Istari type theory, proving theorems using Istari in practice, implementing tactics, applications
Required Background Knowledge
ability to program in ML, type-theoretic sophistication
Course Relevance
PhD students, or undergrads with a interest in advanced programming languages.
Course Goals
The student should know how to prove theorems using Istari.
Learning Resources
The Istari proof assistant
Assessment Structure
class participation 100%
Extra Time Commitment
n/a