CS 6115 (Spring 2015)

Certified Software Systems
TR 8:40-9:55
Hollister 406


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

Course Overview

Part I: Coq Basics

Part II: Certified Systems


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.


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


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:

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:

Validate XHTML Validate CSS
Last updated January 2015