Syllabus

Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as:

• Is this program is correct?
• Will this program produce a run-time type error?
• Can the behavior of two programs be distinguished by an observer?
• Is an optimization a safe program transformation?
• Is it possible for programs written in a language to crash?
• Is a compiler translation correct?
• Can a source language be translated into a given target language?

Topics include:

• Inductive proof
• Operational semantics
• Language features and translation
• Axiomatic semantics
• Denotational semantics
• Type systems

Grading

Evaluation will consist of six homework assignments, a preliminary exam, and a final exam. The breakdown for the overall course grade is as follows:

• Homeworks: 25%
• Preliminary Exams: 30%
• Final Exam: 40%
• Participation: 5%

Homework Policy

Students must complete homework assignments in collaboration with a study group. Late assignments will not be accepted.

Exams

The course will have one preliminary exam and a final exam. Makeup exams must be scheduled within the first two weeks of class. Check now to see if you have a conflict with another class and contact the instructor immediately to reschedule.

Academic Integrity

All students are expected to conduct themselves with the utmost integrity. Academic integrity is rarely an issue in graduate courses, but unfortunately it does arise from time to time, so we want to be clear. Under no circumstances may you hand in work done with or by someone else under your own name or share code or detailed proofs with anyone else except your study group. You may discuss general questions regarding the OCaml language, proof techniques, or the requirements of the assignment with others. Broad hints and general ideas about approaches to a solution are permissible, but if you receive any such hints or ideas from a colleague, you must acknowledge them.

You may not give nor receive assistance from anyone else during an exam. You may not post any code or proof sketch that might be part of a solution on the mailing list.

If you are unsure about what is allowed and what is not, please ask! See here for the university code of academic integrity.

Special Needs and Wellness

We will 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.