Staff
- Instructor: Ranjit Jhala
(rjhala@eng.ucsd.edu) - TA: Michael Borkowski
(mborkows@ucsd.edu) - TA: Cole Kurashige
(ckurashige@ucsd.edu) - TA: Matt Kolosick
(mkolosick@ucsd.edu) - TA: George Sakkas
(gsakkas@ucsd.edu)
Co-ordinates
- Lectures: Tu-Th 12:30 to 1:50pm
- Location: WLH 2005
- Messages: Piazza
Description
The goal of this class is to expose students to advanced programming language ideas, including high-level programming abstractions, expressive type systems and program analyses. We will develop these ideas as follows.
First, we will see how the lambda calculus can be used to distill essence of computation into a few powerful constructs, and we will use it as a launching pad to study expressive type systems, logics and analyses that can make precise predictions about run-time behavior at compile time.
Second, we will study how this calculus yields Haskell, a functional programming language that has been the incubator for many recent PL advances. We will use Haskell to learn about a variety of high-level programming abstractions and techniques.
Third, we will learn how functional programming lends itself to the formal verification of programs, i.e. how to specify that code has certain desirable properties, and how to automatically verify that those properties are indeed satisfied by the implementation.
For more details see the lecture plan.
Prerequisites
The class is mostly self contained. However, it will be helpful to have some knowledge of basic discrete math, and it will be essential that you enjoy programming and have a desire to learn the material.
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; there are no group projects in this course. 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, but you may use Copilot/ChatGPT etc. for your programming assignments.
There will be graded assignments and exam in this course, which will be heavily based on the assignments. 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.