| |
Dec 26, 2024
|
|
|
|
|
CS 5201 - Software Verification
A course on programming languages and software verification, with hands-on exercise in an interactive theorem prover such as Coq. Topics may include, but are not limited to: logic; functional programming; inductive datatypes, recursion, and structural induction; operational, denotational, and axiomatic semantics; simply typed lambda calculus; polymorphic lambda calculus; type systems and type-checking.
Requisites:
Credit Hours: 3
Repeat/Retake Information: May not be retaken.
Lecture/Lab Hours: 3.0 lecture
Grades: Eligible Grades: A-F,WP,WF,WN,FN,AU,I
Learning Outcomes:
- Students will be able to apply higher-order functions, polymorphism, inductive datatypes, and pattern-matching within the context of an interactive theorem prover such as Coq.
- Students will be able to specify and prove properties of small functional programs within an interactive theorem prover such as Coq.
- Students will be able to use operational semantics and Hoare logic in order to reason about small imperative programs.
- Students will be able to reason about and apply basic type systems and type theory in the context of lambda calculi such as the simply typed lambda calculus.
Add to Portfolio (opens a new window)
|
|
