Spring 2023 - CMPT 489 D100

Special Topics in Programming Languages (3)

Semantics and Type Theory

Class Number: 6752

Delivery Method: In Person

Overview

  • Course Times + Location:

    Jan 4 – Apr 11, 2023: Mon, 5:30–6:20 p.m.
    Burnaby

    Jan 4 – Apr 11, 2023: Wed, 4:30–6:20 p.m.
    Burnaby

  • Exam Times + Location:

    Apr 18, 2023
    Tue, 7:00–10:00 p.m.
    Burnaby

  • Prerequisites:

    CMPT 383 with a minimum grade of C-.

Description

CALENDAR DESCRIPTION:

Current topics in programming languages depending on faculty and student interest.

COURSE DETAILS:

This course introduces the fundamental concepts required for formalizing and analyzing programming languages and their logical underpinnings. In this course, we introduce programming languages, their syntax and their semantics, as mathematical objects. Through this treatment, we can then both express and prove precise claims about individual program behavior as well as perform automated analyses on such programs. Throughout this course, we will furthermore introduce students to the interactive theorem prover Coq, which students will use as both a means of programming, proving, and study.

Core topics this course will study include introductions to program syntax and semantics, functional programming, type checking, type inference, type safety, and subtyping.

COURSE-LEVEL EDUCATIONAL GOALS:

Understand how to formally define programming languages
Understand how to build type-systems and prove correctness of type-checking and other forms of automated program analyses
Understand how to use interactive theorem provers

Grading

  • Homework 70%
  • Midterm 1 15%
  • Midterm 2 15%

REQUIREMENTS:

Students who take this class should already have a strong understanding of how to write formal proofs, as well as strong mathematical intuition, and strong programming skills.

Materials

MATERIALS + SUPPLIES:

We will be following the Software Foundations online textbooks throughout this course.

REQUIRED READING NOTES:

Your personalized Course Material list, including digital and physical textbooks, are available through the SFU Bookstore website by simply entering your Computing ID at: shop.sfu.ca/course-materials/my-personalized-course-materials.

Registrar Notes:

ACADEMIC INTEGRITY: YOUR WORK, YOUR SUCCESS

SFU’s Academic Integrity website http://www.sfu.ca/students/academicintegrity.html is filled with information on what is meant by academic dishonesty, where you can find resources to help with your studies and the consequences of cheating. Check out the site for more information and videos that help explain the issues in plain English.

Each student is responsible for his or her conduct as it affects the university community. Academic dishonesty, in whatever form, is ultimately destructive of the values of the university. Furthermore, it is unfair and discouraging to the majority of students who pursue their studies honestly. Scholarly integrity is required of all members of the university. http://www.sfu.ca/policies/gazette/student/s10-01.html