Skip to content
Ranjit Jhala edited this page Jan 16, 2019 · 2 revisions

CSE 230: Proofs of Programs (for Programs, by Programs)

CSE 230 is an introduction to the Formal Semantics of Programming Languages.

Unlike most engineering artifacts, Programming Languages and Programs are mathematical objects whose properties can be formalized. The goal of this course is to introduce students to fundamental intellectual and mechanical tools required to rigorously analyze Languages and Programs and to expose them to recent developments in and applications of these techniques.

We shall study operational and axiomatic semantics, two different ways of precisely capturing the meaning of programs by characterizing their executions. We will see how the lambda calculus can be used to distill essence of computation into a few powerful constructs. We use that as a launching pad to study expressive type systems useful for for analyzing the behavior of programs at compile-time and then, how to derive expressive program analyses using Abstract Interpretation.

All of the above will be done in a concrete fashion, i.e. by writing programs that define the various kinds of semantics, and writing more programs that correspond to proofs about those objects!

Diversity and Inclusion

We are committed to fostering a learning environment for this course that supports a diversity of thoughts, perspectives and experiences, and respects your identities (including race, ethnicity, heritage, gender, sex, class, sexuality, religion, ability, age, educational background, etc.) Our goal is to create a diverse and inclusive learning environment where all students feel comfortable and can thrive.

Our instructional staff will make a concerted effort to be welcoming and inclusive to the wide diversity of students in this course. If there is a way we can make you feel more included please let one of the course staff know, either in person, via email/discussion board, or even in a note under the door. Our learning about diverse perspectives and identities is an ongoing process, and we welcome your perspectives and input.

We also expect that you, as a student in this course, will honor and respect your classmates, abiding by the UCSD Principles of Community.
Please understand that others’ backgrounds, perspectives and experiences may be different than your own, and help us to build an environment where everyone is respected and feels comfortable.

If you experience any sort of harassment or discrimination, please contact the instructor as soon as possible. If you prefer to speak with someone outside of the course, please contact the Office of Prevention of Harassment and Discrimination.

Integrity of Scholarship

University rules on integrity of scholarship will be strictly enforced. By taking this course, you implicitly agree to abide by the UCSD Policy on Integrity of Scholarship described here. In particular,

all academic work will be done by the student to whom it is assigned, without unauthorized aid of any kind.

You are expected to do your own work on all assignments; when specified, you may work in pairs -- but will submit the assignments individually. You may (and are encouraged to) engage in general discussions with your classmates regarding the assignments, but specific details of a solution, including the solution itself, must always be your own work.

There will be graded assignments and exam in this course, as described below. All exams are closed book; no tools other than your brain and a writing instrument are to be used.

Incidents which violate the University's rules on integrity of scholarship will be taken seriously. In addition to receiving a zero (0) on the assignment/exam in question, students may also face other penalties, up to and including, expulsion from the University. Should you have any doubts about the moral and/or ethical implications of an activity regarding the course, please see the instructor.

Research

Your class work might be used for research purposes. For example, we may use anonymized student assignments to design algorithms or build tools to help programmers. Any student who wishes to opt out can contact the instructor or TA to do so after final grades have been issued. This has no impact on your grade in any manner.

Clone this wiki locally