Basic Information
The Course Consists of Two Major Parts# 1. Automated Reasoning# Methods and Tools For Formal Reasoning Of Computer Programs and Formal Semantics of Programming Languages. Topics Include# Lambda Calculus, Type Checking, Polymorphism, Type Theory, Formalizing Programs in First-order Logic, Satisfiability Modulo Theory. 2. Program Synthesis# Automatic Generation of Program Code By a Synthesizing Compiler. Topics Include# Syntax-guided Syntheis, Programming By Examples, Counterexample-guided Inducive Syntheis, Type-directed and Deductive Synthesis. Learning Outcomes# By The End of The Course, Students Will# 1.understand The Mathematical Construction of Formal Proofs From First Principles, and The Difference Between Formal Proofs and "ordinary" Pen-and-paper Proofs. 2.be Familiar With The Terms Constructive Logic and Martin-loef Type Theory, Especially How They Differ From Classical Logic(s), and The Proofs-as-programs Correspondence. 3. Develop Skills For Proving Logical Propositionsusing Using The Coq Proof Assistant, a Tool For Mechanical Formulation of Proofs Based On Dependent Types. 4. Learn To Formalize Properties of Computer Programs Using Two Widely Acepted Forms of Semantics# Operational and Exiomatic Semantics and Prove Such Properties Using Both Manually (in Coq) and Automatically (using Smt Solvers) 5. Know The Taxonomy of Software Syntheis Techniques And Representative Algorithms. 6. Experience Program Synthesis Using Synthesis Tools# Sketch and Synquid. 7. Design and Code a Software Synthesis Tool From The Grounds Up, Based On Algorithms And Optimizations Acquired in Class, As Part of a Final Project.
Faculty: Computer Science
|Undergraduate Studies
|Graduate Studies
Parallel course
236360 - Theory of Compilation