Abstract:Title: The Coq proof assistant is an environment for developing mathematical proofs. In practice, it is used to write formal specifications, programs, and proofs to ensure programs adhere to their specifications. These specifications, programs, and proofs are formalized in the Calculus of Inductive Constructions (CIC), which is a powerful formal language. Logical judgments are then performed by a trusted kernel through type-checking. Theorem proving in Coq is an interactive, often difficult process, where programmers provide a proof tactic to try (such as induction), Coq tries to search for a proof term (whose type is the theorem itself), and then Coq outputs feedback on the current state of the proof.
In this talk, I will give an overview of the Coq proof assistant, including its foundations, notable applications, and techniques for automating the theorem proving process in Coq (which is where my research lies).
The CICS Theory Seminar is online, free and open to the public. If you are interested in giving a talk, please email Professor Immerman or Rik Sengupta. Note that in addition to being a public lecture series, this is also a one-credit graduate seminar (CompSci 891M) that can be taken repeatedly for credit.