Special Topics in Computer Science
COMP 360
Spring 2016
| Section:
01
02
|
| This course may be repeated for credit. |
| Crosslisting:
COMP 560 |
Topics vary by offering; recent topics have included information theory, advanced algorithms, and logic programming. |
|
| Credit: 1 |
Gen Ed Area Dept:
NSM MATH |
| Course Format: Lecture | Grading Mode: Graded |
| Level: UGRD |
Prerequisites: COMP212 |
|
Fulfills a Requirement for: (COMP)(MATH)(NS&B)(STS) |
|
Past Enrollment Probability: 75% - 89% |
| SECTION 01 | | Special Attributes: CQC |
Major Readings: Wesleyan RJ Julia Bookstore
To be announced.
|
Examinations and Assignments:
Students will be assessed by homework assignments and by an end-of-semester project, where they will write a computer-checked program or proof of their choice. |
Additional Requirements and/or Comments:
Undergraduates may take this course up to two times for a letter grade and up to four times for credit towards graduation.
Computer-Checked Programs and Proofs There is a strong correspondence between mathematics and programming, under which mathematical proofs correspond to programs. A _proof assistant_ is a tool that a mathematician/programmer can use to represent proofs/programs, in such a way that a computer can verify whether or not they are correct. The use of proof assistants in math and computer science is becoming ever more important for managing the increasing complexity of proofs and programs. Proof assistants have been used to check significant mathematical theorems, such as the Four Color Theorem and the Feit-Thompson Odd-Order Theorem, as well as large pieces of software, such as a C compiler and the definition of the Standard ML programming language. In this course, students will learn to use the Agda proof assistant to write computer-checked programs and proofs. |
| Instructor(s): Licata,Dan Times: ..T.R.. 10:30AM-11:50AM; Location: SCIE141; |
| Total Enrollment Limit: 30 | | SR major: 10 | JR major: 10 | | |
| Seats Available: 0 | GRAD: X | SR non-major: 0 | JR non-major: 0 | SO: 10 | FR: 0 |
| Drop/Add Enrollment Requests | | | | | |
| Total Submitted Requests: 0 | 1st Ranked: 0 | 2nd Ranked: 0 | 3rd Ranked: 0 | 4th Ranked: 0 | Unranked: 0 |
| SECTION 02 | | Special Attributes: CQC |
Major Readings: Wesleyan RJ Julia Bookstore
Same as Section 01 Above |
Examinations and Assignments:
TBA |
Additional Requirements and/or Comments:
Automated theorem proving:
The content on this course will be first focused about automated theorem proving, a fundamental tool for formalization in mathematics and software engineering. We will review the tableaux method, resolution and SAT solvers, with an extension to SMT-solver, the state-of-the art prover for first-order logic. We will also cover the completeness and soundness theorems for those proving methods, that are the two results on which the above described proof-systems rely: everything that is true is provable (completeness) and that everything that is proved is true (soundness).
In the second half, we will see that those theorems have a somehow unexpected impact on the semantics of programs through the proof-as-programs correspondence, and that they give rise to normalization algorithms for the typed lambda-calculus. For this, we shall study typed lambda-calculus, normalization proofs and realizability, a mean to give computational content to mathematical proofs.
Other topics, such as classical realizability, resulting forcing models, linear logic, game semantics, implicit complexity or quantum programming languages, etc will be the subject of a final presentation by students. |
| Instructor(s): Hermant,Olivier M. Times: ..T.R.. 02:40PM-04:00PM; Location: SCIE137; |
| Total Enrollment Limit: 30 | | SR major: 10 | JR major: 10 | | |
| Seats Available: 23 | GRAD: X | SR non-major: 0 | JR non-major: 0 | SO: 10 | FR: 0 |
| Web Resources: Syllabus |
| Drop/Add Enrollment Requests | | | | | |
| Total Submitted Requests: 0 | 1st Ranked: 0 | 2nd Ranked: 0 | 3rd Ranked: 0 | 4th Ranked: 0 | Unranked: 0 |
|
|