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-1033 **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.

UndergraduatesAssignments 50% Participation/Preparedness 10% Midterm exam 15% Final exam 25%

Graduate studentsAssignments 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.