ITU CISAT
  • Research
  • Courses
  • Projects
  • People
  • News & Events
  • About
  • Contact

← All courses

Substructural Logics

Overview 1. Truth is Ephemeral 2. Connectives 3. Cut-elimination 4. Proof Terms and Message Passing 5. The MPASS language 6. Preservation, Progress, and Subtyping 7. Validity 8. Mixed Logic 9. Adjoint Logic 10. Focusing 11. Programming in Sax

Substructural Logics

3. Cut-elimination

Course notes:

We follow Frank’s course notes and prove cut-elimination for ordered logic. (https://www.cs.cmu.edu/~fp/courses/15836-f23/lectures/03-cutelim.pdf)

Additional Reading

Exercises

Assignment 2: (https://www.cs.cmu.edu/~fp/courses/15836-f23//assignments/hw2.pdf)

Previous ← 2. Connectives Next 4. Proof Terms and Message Passing →

© 2026 ITU CISAT · IT University of Copenhagen · Rued Langgaards Vej 7, DK-2300 Copenhagen S