Course materials for UCSD CSE 230, Winter 2019
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!
- Lectures: MWF 1:00p-1:50p in WLH 2113
- Final: Take home during finals week
- Announcements: On Piazza
- Functional Programming e.g. CSE 130
There is no text for CSE 230, but we will be basing much of the material on:
| Week | Topic | Code | Link |
|---|---|---|---|
| 1. | Refinement Types | lhs | tutorial |
| Proofs of Programs | |||
| 2. | Programs as Proofs | lhs | Ch2 of Nipkow & Klein |
| 3. | Induction on Terms | lhs | Ch3 of Nipkow & Klein |
| 4. | Induction on Evidence | lhs | Ch4 of Nipkow & Klein |
| Proofs for Programs | |||
| 5. | Big Step Semantics | lhs | Ch7 of Nipkow & Klein |
| 6. | lhs | ||
| 7. | Small Step Semantics | lhs | |
| 8. | lhs | ||
| 9. | Axiomatic Semantics | lhs | |
| 10. | lhs | ||
| Type Systems | |||
| Proofs by Programs | |||
| Horn Clauses | |||
| Abstract Interpretation | |||
| Refinement Types | |||
- Can be found here
All announcements are on on Piazza
Involves in class participation and answering questions on Piazza.
- There will be a total of 5-6
- You have a total of four late days
- They may be done in pairs
A late day can be used for any programming assignment and is anything between 1 second and 23 hours 59 minutes and 59 seconds after the deadline.
- Produce LaTeX lecture notes for one lecture
- Due one week after the lecture
- They may be done in pairs
- Stay tuned for signup form and template
- This will be a "take home" exam
- Run during finals week.
- Haskell-Lang
- Getting started with Haskell
- What I Wish I Knew When Learning Haskell
- Haskell Cheat Sheet
- Haskell Pitfalls
- Haskell Programming from First Principles by Christopher Allen and Julie Moronuki
- Programming in Haskell by Graham Hutton
- Real World Haskell by Bryan O' Sullivan, John Goerzen, and Don Stewart
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.
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.
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.