A printable PDF is available.

CSC 495/693 Class Information and Syllabus

Instructor: Stephen R. Tate (Steve)
Lectures: Tues/Thurs 5:30-6:45, Petty 150
Office: Petty 166
Office Hours: Tues/Thurs 10:00-11:30, or by appointment
Phone: 336-256-xxxx [old number]
E-mail:

Class Web Site: http://www.uncg.edu/cmp/faculty/srtate/495/

Textbook (online and free):

Benjamin C. Pierce, et al. Software Foundations,
https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

This is an online textbook that has embedded exercises that can be worked in the Coq Interactive Theorem Prover. Students should use the copy on our class web site which is guaranteed not to change for the duration of the class. More information on how to work with this text will be given in class.

Software (online and free): This course uses the Coq Proof Assistant, available online at https://coq.inria.fr/. Coq is available on UNCG lab computers through the "mycloud" service. For consistency, we will always use version 4.5pl1 (note that Coq can be sensitive to version numbers - make sure your solutions work with this version!).

Brief Description: This course explores logic and tools used to reason about software correctness, developing student skills to produce higher quality and more robust software. By the end of the course, students will be capable of working on small to medium scale projects, which can lead to a future project that is suitable for an honors project, masters project, or masters thesis. This course will also provide the background needed to work as a research assistant in an active research program, for students interested in advancing the field in this area.

Prerequisites: C or better in CSC 330 required. It is strongly recommended that students should have completed CSC 339 and CSC 350. Here's how the authors of the textbook describe the background they assume for readers of their book: "The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful." Note that "mathematical maturity" includes the requirement that students are comfortable with the overlapping notions of induction, recursion, and proofs.

Class Structure: Students in this class will follow a three-phase "prepare/discuss/finish" learning process for each topic covered in the class. Students are expected to read the entire chapter for each topic before it is discussed in class, and must make their best effort to solve all one-star problems in the chapter before the class discussion. Students should bring laptops to class if possible, and class time will be used for collaborative problem solving and discussion. Students will be called on to show and explain the solutions they derived (for pre-class or in-class work) using the classroom ShareLink technology, which allows students to show their laptop screen on the classroom projector. After the class discussion, students must finish the exercises in the chapter (some exercises may be excluded by the instructor, and some additional problems may be assigned). For each week's material, solutions are due the following Thursday at midnight.

Assignments and Student Work: Coq must accept the entire file on any work submitted (this is the Coq equivalent of "your code must compile without errors"). For problems you are unable to complete, use the Coq "Admitted" command or "admit" tactic to tell Coq to skip past your incomplete solution. Solutions will be turned in electronically, and instructions on how to submit will be provided before the first assignment. Solutions will be graded not only for correctness, but also for elegance and style of proofs.

Late Policy for Assignments: Assignments are due every Thursday at midnight, and may be turned in up to 7 calendar days late with a 25% late penalty. Students with planned absences, whether for university events, religious observance, or other reason, are expected to make arrangements with the instructor to turn in assignments or take exams before the scheduled date of the assignment or test. No assignment will be accepted more than 7 calendar days after the original due date!

Exams: There will be one midterm exam, the date of which will be announced at least two weeks in advance, and a final exam, which will be held at the university-scheduled time (Tuesday, December 13, 7:00-10:00 P.M.). A missed exam may be made up only if it was missed due to an extreme emergency and arrangements are made before the exam date. Exams (including the final) may not be taken early or late due to personal travel plans.

Attendance/Participation Policy: This class is heavily dependent on discussion and participation, and students are expected to come to class prepared every day, having read the necessary material and attempted all one-star problems. Points will be deducted from the "Participation/Preparedness" portion of the grade for each missed or unprepared-for class (with two "freebies"). The university allows for a limited number of excused absences for religious observances -- students who plan to take such an absence should notify the instructor at least two weeks in advance so that accommodations can be made (see the late work policy above). It is the student's responsibility to obtain notes from another student if they miss class.

Graduate Students in CSC 693: Students registered in CSC 693 will be required to complete an independent self-directed project during the last month of the class (concurrent with other class work). More information will be provided later in the semester.

Evaluation and Grading: Each student activity will contribute to the final grade in the class according to the following percentages.

Undergraduates
Assignments	50%
Participation/Preparedness	10%
Midterm exam	15%
Final exam	25%

 

Graduate students
Assignments	40%
Participation/Preparedness	10%
Midterm exam	15%
Final exam	25%
Project	10%

Topics and Schedule: See the schedule on the class web site.

Academic Integrity: Students are required to abide by the UNCG Academic Integrity Policy on all work. For information on the UNCG Academic Integrity Policy, see the UNCG Academic Integrity web site at http://academicintegrity.uncg.edu/.

Assignments in this class are for individual work, unless explicitly stated otherwise. General concepts and material covered in the class may be discussed with other students or in study groups, but specific assignments should not be discussed and any submitted work should be done entirely your own - never be copied from the Internet or from another student.

Any incidents of academic dishonesty will be handled strictly, resulting in either a zero on the assignment or an F in the class, depending on the severity of the incident, and incidents will be reported to the appropriate UNCG office.

In-class Behavior: When you are in class you should be focused on the class, and you should act in a professional and mature manner. During class there should be no eating, drinking, e-cigarettes, cellphone use, non-class related laptop use, or anything else that does not pertain to the class activities. Any distracting items may be confiscated at the discretion of the instructor.

ADA Statement: UNCG seeks to comply fully with the Americans with Disabilities Act (ADA). Students requesting accommodations based on a disability must be registered with the Office of Accessibility Resources and Services located in 215 Elliott University Center: (336) 334-5440 (or http://oars.uncg.edu).

University Closings: If university facilities are closed due to flu outbreak or other emergencies, it does not mean that classes are canceled. In such an event, please check the class web page and Canvas site for information about if and how the class will proceed.