Course Syllabus

Jump to Today

Syllabus

CS 7936: Seminar: Type Theory Foundations

WEB 2460, M 13:25-14:45

(livestreamed and recorded via Zoom)

Instructors

Instructor:

Ben Greenman <blg@cs.utah.edu> MEB 3252

Course Description

Overview

Course CS 7936
Department School of Computing
Credit Hours 1
Semester Spring 2025
Outcomes Learn about fundamental and late-breaking research in type systems and constructive math.

Goals & Objectives

  • Read deeply about types, logics, proofs, inference, and programming languages.
  • Present research results.
  • Engage in class discussions, learn to ask insightful and actionable questions.

This semester (Spring 2026) we will read about Model Theory. In the words of Dirk van Dalen:

"if proof theory is about the sacred, then model theory is about the profane."

We will fearlessly read one chapter per week until we finish the book. After that, we'll go back to earlier exercises and read papers that apply model theory to type theory.

Why model theory? Many ideas from model theory are useful in type theory and beyond:

  • Bisimulation invariance is useful for proving that two programs are equal (e.g., to show that an optimizing compiler is correct).
  • SMT solvers use quantifier elimination in fast decision procedures.
  • Program logics (Hoare logic, Separation logic) are interpreted over program models.
  • Curry-Howard relates truth-value semantics (model theory) to type-theoretic syntax (proof theory).
  • Proofs of completeness (i.e., every true fact about a program is expressible in my proof system) may use model theory. Example: [Journal of Logic and Computation, 2021]
  • EF games, Pebble games, and more can prove lower bounds on the expressiveness of bounded-depth circuits, restricted proof systems, etc.

Thanks to ChatGPT for providing an initial list of 30 bullets that I boiled down to the above.

Materials

Free to read online from campus or VPN.

Communication

Discord:

Email:

Office Hours

By appointment. Email Ben.

Evaluation

  • Grading is based on sincere participation in course activities. Core activities are:
    • reading papers
    • presenting papers
    • attending class
    • contributing to class discussions
  • Students may also do a research project. The instructor will meet weekly with each student to discuss the project. Project suggestions:
    • Model a research paper in Redex
    • Replicate the algorithm / experiments from a paper
    • Apply insights from a paper to your Ph.D. topic

The instructor will reach out early and often to students who are not participating enough. Students who are concerned about their grade should contact the instructor.

Course Policies

  • Read together. Ask questions. It's good. It's encouraged.
  • Do your own work on the projects.
  • Late assignments are not accepted
  • Remote participation is not allowed.

Support

Accommodations will be considered on an individual basis and may require documentation.

Please contact your instructor and/or teaching assistant as soon as possible (preferably shortly before the semester begins) to request accommodations of any kind.

Contact your instructor as soon as possible if an extreme personal circumstance
(hospitalization, death of a close relative, natural disaster, etc.) is interfering with your ability to
complete your work.

To request an accommodation for religious practices, contact your instructor at the beginning of the semester.

If you are student on active duty with the military and experience issues that prevent you from participating in the course because of deployment or service responsibilities, contact your instructor as soon as possible to discuss appropriate accommodations.

Disability Access

All written information in this course can be made available in an alternative format with prior notification to the Center for Disability Services (CDS). CDS will work with you and the instructor to make arrangements for accommodations. Prior notice is appreciated. To read the full accommodations policy for the University of Utah, please see Section Q of the Instruction & Evaluation regulations.

If you will need accommodations in this class, contact:

Center for Disability Services
801-581-5020
disability.utah.edu
162 Union Building
    200 S. Central Campus Dr.
     Salt Lake City, UT 84112

Office of Equal Opportunity

The Office of Equal Opportunity And Affirmative Action (OEO/AA) is dedicated to providing a fair and equitable environment for all to pursue their academic and professional endeavors and to equally access University programs.

OEA/AA
801-581-8365
oeo.utah.edu
383 South University Street
    Level 1, OEO Suite
    Salt Lake City, UT 84112

Price College Counseling Service

Goal: provide a confidential, safe, and non-judgmental space to address any stressor or concern in your life. Empower you to take actions to meet your needs, values, and goals.

Call to schedule an Initial Consultation (IC) appointment. Be sure to ask for “embedded counseling for College of Engineering”.

Counseling Center
801-581-6826
www.price.utah.edu/students/current/counseling
WEB 1707

University Policies

Americans with Disabilities Act (ADA)

The University of Utah seeks to provide equal access to its programs, services, and activities for people with disabilities.

All written information in this course can be made available in an alternative format with prior notification to the Center for Disability & Access (CDA). CDA will work with you and the instructor to make arrangements for accommodations. Prior notice is appreciated. To read the full accommodations policy for the University of Utah, please see Section Q of the Instruction & Evaluation regulations.

In compliance with ADA requirements, some students may need to record course content. Any recordings of course content are for personal use only, should not be shared, and should never be made publicly available. In addition, recordings must be destroyed at the conclusion of the course.

If you will need accommodations in this class, or for more information about what support they provide, contact:

Center for Disability & Access

  801-581-5020
  disability.utah.eduLinks to an external site.
 Third Floor, Room 350
 Student Services Building
 201 S 1460 E
 Salt Lake City, UT 84112

Safety at the U

The University of Utah values the safety of all campus community members. You will receive important emergency alerts and safety messages regarding campus safety via text message. For more safety information and to view available training resources, including helpful videos, visit safeu.utah.edu.

To report suspicious activity or to request a courtesy escort, contact:

Campus Police & Department of Public Safety

  801-585-COPS (801-585-2677)
  dps.utah.edu
  1735 E. S. Campus Dr.
  Salt Lake City, UT 84112

Addressing Sexual Misconduct

Title IX makes it clear that violence and harassment based on sex and gender (which includes sexual orientation and gender identity/expression) is a civil rights offense subject to the same kinds of accountability and the same kinds of support applied to offenses against other protected categories such as race, national origin, color, religion, age, status as a person with a disability, veteran’s status, or genetic information.

If you or someone you know has been harassed or assaulted, you are encouraged to report it to university officials: 

Title IX Coordinator & Office of Equal Opportunity and Affirmative Action

  801-581-8365
  oeo.utah.edu
  135 Park Building
  201 Presidents' Cir.
  Salt Lake City, UT 84112

Office of the Dean of Students

  801-581-7066
  deanofstudents.utah.edu
  270 Union Building
  200 S. Central Campus Dr.
  Salt Lake City, UT 84112

To file a police report, contact:

Campus Police & Department of Public Safety

  801-585-COPS (801-585-2677)
  dps.utah.edu
  1735 E. S. Campus Dr.
  Salt Lake City, UT 84112

If you do not feel comfortable reporting to authorities, the U's Victim-Survivor Advocates provide free, confidential, and trauma-informed support services to students, faculty, and staff who have experienced interpersonal violence.

To privately explore options and resources available to you with an advocate, contact:

Center for Student Wellness

  801-581-7776
  wellness.utah.edu
 350 Student Services Building
 201 S. 1460 E.
 Salt Lake City, UT 84112

Academic Misconduct

It is expected that students comply with University of Utah policies regarding academic honesty, including but not limited to refraining from cheating, plagiarizing, misrepresenting one’s work, and/or inappropriately collaborating. This includes the use of generative artificial intelligence (AI) tools without citation, documentation, or authorization. Students are expected to adhere to the prescribed professional and ethical standards of the profession/discipline for which they are preparing. Any student who engages in academic dishonesty or who violates the professional and ethical standards for their profession/discipline may be subject to academic sanctions as per the University of Utah’s Student Code: Policy 6-410: Student Academic Performance, Academic Conduct, and Professional and Ethical Conduct.

Plagiarism and cheating are serious offenses and may be punished by failure on an individual assignment, and/or failure in the course. Academic misconduct, according to the University of Utah Student Code:

“...Includes, but is not limited to, cheating, misrepresenting one’s work, inappropriately collaborating, plagiarism, and fabrication or falsification of information…It also includes facilitating academic misconduct by intentionally helping or attempting to help another to commit an act of academic misconduct.”

For details on plagiarism and other important course conduct issues, see the U's Code of Student Rights and Responsibilities.

Course Summary:

Course Summary
Date Details Due