Syllabus

A hands-on introduction to programming using the Coq proof assistant.

Course Overview

Part I: Coq Basics

• Operational, denotational, and axiomatic semantics
• λ-calculus

Part II: Certified Systems

• Compilers
• Operating systems
• Web browsers

Announcements

We will use Piazza, a web-based forum, for communication with classmates and the course staff and online discussion. You can sign up at http://www.piazza.com/cornell/spring2015/cs6115. You are responsible for familiarizing yourself with all announcements made on Piazza.

The instructor will frequently monitor the forum and will respond to questions in a timely manner. This is the most efficient method of getting help and has the added advantage that others can benefit from your question.

Grading

Evaluation will consist of participation and two projects, one smaller and one larger. The breakdown for the overall course grade is as follows:

• Participation: 50%
• Small Project: 10%
• Final Project: 40%

Exams

The course will not have exams.

Academic Integrity

Absolute integrity is expected of all Cornell students in every academic undertaking. The course staff will prosecute violations aggressively using automatic detection tools.

You are responsible for understanding every word of these policies:

• Cornell University Code of Academic Integrity
• Computer Science Department Code of Academic Integrity

The protocol for prosecution of violations is described here: Explanation of AI Proceedings.

Under no circumstances may you hand in work done with or by someone else under your own name or share code with anyone else unless explicitly allowed.

If you are unsure about what is permissible and what is not, please ask!

Special Needs and Wellness

It is university policy to provide reasonable accommodations to students who have a documented disability (e.g., physical, learning, psychiatric, vision, hearing, or systemic) that may affect their ability to participate in course activities or to meet course requirements. Students with disabilities are encouraged to contact Student Disability Services at 607-254-4545, or the instructor for a confidential discussion of their individual needs.

If you are experiencing undue personal or academic stress at any time during the semester or need to talk to someone who can help, contact the instructor or:

• Engineering Academic Advising at 607-255-7414,
• Learning Strategies Center at 607-255-6310,
• Let's Talk Drop-in Counseling at Gannett at 607-255-5155
• Empathy Assistance and Referral Service at 607-255-EARS.