Git Product home page Git Product logo

230-wi19-web's Introduction

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

Course materials for UCSD CSE 230, Winter 2019

Course Description

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!

Co-ordinates

  • Lectures: MWF 1:00p-1:50p in WLH 2113
  • Final: Take home during finals week
  • Announcements: On Piazza

Staff

Calendar

Prerequisites

  • Functional Programming e.g. CSE 130

Text

There is no text for CSE 230, but we will be basing much of the material on:

Proofs of Programs, for Programs, by Programs

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
Proofs for Programs
5. Operational Semantics
6. Axiomatic Semantics
7. Type Systems
Proofs by Programs
8. Horn Clauses
9. Abstract Interpretation
10. Refinement Types

Grading

Class Participation (10%)

Involves in class participation and answering questions on Piazza.

Programming Assignments (45%)

  • 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.

Scribe Notes (20%)

  • 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

Final (25%)

  • This will be a "take home" exam
  • Run during finals week.

Links

LiquidHaskell

Getting Started with Haskell

Books on Haskell

Miscellaneous

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.

230-wi19-web's People

Contributors

anilkyelam avatar audrey-randall avatar kellianhunt avatar michaelborkowski avatar mossaka avatar ranjitjhala avatar

Watchers

 avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.