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
