Introduction to computer-assisted proof

NámsgreinT-733-ICAP
Önn20243
Einingar6
SkyldaNei

Ár1. ár
ÖnnHaustönn/Fall 2024
Stig námskeiðsÓskilgreint
Tegund námskeiðsValnámskeið
UndanfararT-117-STR1, Strjál stærðfræði I
Skipulag3 week,Theory course
Kennari
Tarmo Uustalu
Lýsing
How to obtain documented and checkable assurance that a program does the right thing? This course is an introduction to the trustworthiness technology of computer-assisted proof. The main underpinning principles of technology are introduced as well as the proof assistant Agda as a tool in which algorithms and data structures can be programmed and proved correct at the same time. Intro to programming and proving in the proof assistant Agda: basic typed functional programming in Agda (higher-order functions, polymorphism, datatypes), Curry-Howard correspondence ("propositions as types, proofs as programs") and logic, dependent types, dependent function and dependent pair types, the identity type. First examples of proofs about programs (properties of various list functions). Datatypes with invariants (vectors, sorted lists, binary search trees), programming with them, proving programs with them correct. An overview of the state-of-the-art in computer-assisted proof (interactive and fully automatic provers), major projects of formalized computer science and mathematics.
Námsmarkmið
Knowledge: The learner understands the "propositions as types, proofs as programs" correspondence, knows the basics of dependent type theory. Skills: The learner can code simple data structures and algorithms in the proof assistant Agda and prove them to have the desired properties. Competence: The learner appreciates the importance of formal specification and proof for trustworthiness of IT systems, has a high-level picture of the state-of-the-art in computer-assisted proof and its applications in computer science and mathematics.
Námsmat
Attendance/active participation in class 20%, assignments 40%, small project 40%
Lesefni
Ekkert skráð lesefni.
Kennsluaðferðir
Lectures/demo sessions 48 hours, reading/independent practice 30 hours, assignments/small project 72 hours, Total: 150 hours
TungumálEnska