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 Major 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 endofsemester project, where they will write a computerchecked 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.
ComputerChecked 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 FeitThompson OddOrder 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 computerchecked programs and proofs. 
Instructor(s): Licata,Dan Times: ..T.R.. 10:30AM11:50AM; Location: SCIE141; 
Total Enrollment Limit: 30   SR major: 10  JR major: 10   
Seats Available: 0  GRAD: X  SR nonmajor: 0  JR nonmajor: 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 SMTsolver, the stateofthe art prover for firstorder logic. We will also cover the completeness and soundness theorems for those proving methods, that are the two results on which the above described proofsystems 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 proofasprograms correspondence, and that they give rise to normalization algorithms for the typed lambdacalculus. For this, we shall study typed lambdacalculus, 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:40PM04:00PM; Location: SCIE137; 
Total Enrollment Limit: 30   SR major: 10  JR major: 10   
Seats Available: 23  GRAD: X  SR nonmajor: 0  JR nonmajor: 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 

