Simon Fraser University
Engaging the World

Course Outlines

Spring 2023 - CMPT 980 G100

Special Topics in Computing Science (3)

Semantics and Type Theory

Class Number: 6939

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:

    Instructor discretion.

Description

CALENDAR DESCRIPTION:

This course aims to give students experience to emerging important areas of computing science.

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.

Graduate Studies Notes:

Important dates and deadlines for graduate students are found here: http://www.sfu.ca/dean-gradstudies/current/important_dates/guidelines.html. The deadline to drop a course with a 100% refund is the end of week 2. The deadline to drop with no notation on your transcript is the end of week 3.

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