doodle

CSE 230: Principles of Programming Languages CSE 230

Resources - Assignments - Schedule - Grading - Policies

Summary

CSE 230 is an introduction to the Semantics of Programming Languages. Unlike most engineering artifacts, programming languages and hence, programs are mathematical objects whose properties can be formalized. The goal of CSE 230 is to to introduce you to the fundamental mental and mechanical tools required to rigorously analyze languages and programs and to expose you 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.

We will study all of the above in the context of lean, an interactive proof assistant that will help us precisely formalize and verify our intuitions about languages and their semantics.

Students will be evaluated on the basis of 4-6 programming (proving!) assignments, and a final exam.

Prerequisites

Basic functional programming e.g. as taught in UCSD CSE 130 using languages like Haskell, OCaml, Scala, Rust, and undergraduate level discrete mathematics, i.e. logic, sets, relations.

Basics

  • Lecture: WLH 2005 TuTh 12:30p-1:50p
  • Final Exam: 03/18/2025 Tu 11:30a-2:29p
  • Podcasts: podcast.ucsd.edu
  • Piazza: Piazza

Staff and Office Hours

  • Ranjit Jhala: Tu, Th 2-3p (3110)
  • Nico Lehmann: Th 3:30pm-5:00pm (Zoom), Fr 9:30am-11am (B240A), Zoom link in canvas
  • Naomi Smith: Tu 12pm-3pm (Zoom)
  • Matt Kolosick: Mo 10am-12pm (Zoom), Thursday 10am-11am (Zoom)
  • Mingyao Shen: We 12-1p (B240A)
  • Kyle Thompson: Mo 1-2p (B260A)

Please check the CANVAS calendar before you come in case there have been any changes.

Resources

The course is loosely based on Concrete Semantics but there is no official textbook; we will link to any relevant resources that may be needed to supplement the lecture material.

Some other useful links are:

Assignments

  1. Assignment X - Github/ID due 1/17
  2. Assignment 0 - Induction due 1/22

Schedule

The schedule below outlines topics, due dates, and links to assignments. The schedule of lecture topics might change slightly, but I post a general plan so you can know roughly where we are headed.

Week 1 - Basics and Induction

Week 2 - Expressions and Evidence

Week 3 - Big Step Semantics

  • Induction on Evidence (Ch04)
  • Imperative Programs: States, Commands, Transitions
  • Program Equivalence (Ch07)

Week 4 - Small Step Semantics

  • Preservation and Progress (Ch09)

Week 5, 6 - Axiomatic Semantics

  • Assertions, Floyd-Hoare Logic, Soundness (Ch12)
  • Verification Conditions and Automatic Verification

Week 7, 8 - Simply Typed Lambda Calculus

  • Terms, Types, and Typing Rules
  • Denotational Semantics and Type Soundness

Week 9, 10 - Automated Verification

  • Satisfiability Modulo Theories
  • Flux: Refinement Type based verification for Rust

Grading

Your grade will be calculated from assignments, exam, and participation

  • Participation Quizzes (15%) Most lectures will come with a 1-2 page handout, and you can submit the handout any time up until the start of the next lecture. Credit is given for reasonable effort in engaging with the material from the day on the handout.

  • Programming Assignments (40%) There will be a total of 5-6 programming assigments, to be done in pairs but submitted individually.

  • In Class Exams (45%) We will have three "in-class exams" Th 1/30 and Tu 2/25 and Th 3/13 each worth 15% of the grade.

Comprehensive Exam: For graduate students using this course for a comprehensive exam requirement, you must get "A" achievement on the exams.

Policies

All assignments are Closed collaboration assignments, where you cannot collaborate with others (except your partner). Of course you can ask questions on Piazza, and come to office hours etc. In particular,

  • You cannot look at or use anyone else's code for the assignment
  • You cannot discuss the assignment with other students
  • You cannot post publicly about the assignment on the course message board (or on social media or other forums). Of course, you can still post questions about material from lecture or past assignments!

You should be familiar with the UCSD guidelines on academic integrity as well.

Late Work

You have a total of six late days that you can use throughout the quarter, but no more than four late days per assignment.

  • A late day means anything between 1 second and 23 hours 59 minutes and 59 seconds past a deadline
  • If you submit past the late day limit, you get 0 points for that assignment
  • There is no penalty for submitting late but within the limit

Regrades

Mistakes occur in grading. Once grades are posted for an assignment, we will allow a short period for you to request a fix (announced along with grade release). If you don't make a request in the given period, the grade you were initially given is final.

Laptop/Device Policy in Lecture

There are lots of great reasons to have a laptop, tablet, or phone open during class. You might be taking notes, getting a photo of an important moment on the board, trying out a program that we're developing together, and so on. The main issue with screens and technology in the classroom isn't your own distraction (which is your responsibility to manage), it's the distraction of other students. Anyone sitting behind you cannot help but have your screen in their field of view. Having distracting content on your screen can really harm their learning experience.

With this in mind, the device policy for the course is that if you have a screen open, you either:

  • Have only content onscreen that's directly related to the current lecture.
  • Have unrelated content open and sit in one of the back two rows of the room to mitigate the effects on other students. I may remind you of this policy if I notice you not following it in class. Note that I really don't mind if you want to sit in the back and try to multi-task in various ways while participating in lecture (I may not recommend it, but it's your time!)

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 (https://ucsd.edu/about/principles.html). 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: https://ophd.ucsd.edu/.