Logical Foundations of Programming Languages (2020-2021)

Proofs part

Course 1

• blackboard copy
• course notes pages 9-14

Course 2

• blackboard copy
• course notes pages 16-19
• Homework: prove correctness and completeness of LK with implication only (use completeness of Hilbert's system)

Course 3

• blackboard copy
• course notes pages 20-24

Course 4

• blackboard copy
• course notes pages 24-25, 29-36, 85-86
• Homework: prove the following properties, or justify why they are not provable (we admit that cut-elimination holds)
  1. A ⊢ A ⊗ A
  2. A ⊢ A & A
  3. A ⊢ A ⅋ A
  4. A ⊢ A ⊕ A
  5. A ⊗ B ⊢ B ⊗ A
  6. A ⊕ B ⊢ B ⊕ A
  7. (A ⅋ B) ⅋ C ⊢ A ⅋ (B ⅋ C)
  8. A ⊗ (B ⅋ C) ⊢ (A ⊗ B) ⅋ C
  9. (A ⊗ B) ⅋ C ⊢ A ⊗ (B ⅋ C)
  10. (A ⅋ A^⊥) ⊗ (A ⅋ A^⊥) ⊢ A ⅋ A^⊥
  11. (A ⊗ B) & (A ⊗ C) ⊢ A ⊗ (B & C)
  12. A ⊗ (B & C) ⊢ (A ⊗ B) & (A ⊗ C)
  13. (A ⅋ B) & (A ⅋ C) ⊢ A ⅋ (B & C)
  14. A ⅋ (B & C) ⊢ (A ⅋ B) & (A ⅋ C)
  15. (A ⅋ B) ⊕ (A ⅋ C) ⊢ A ⅋ (B ⊕ C)
  16. A ⅋ (B ⊕ C) ⊢ (A ⅋ B) ⊕ (A ⅋ C)
  17. A ⊗ 1 ⊢ A
  18. A ⅋ 1 ⊢ A
  19. A ⊗ 0 ⊢ 0
  20. A & 0 ⊢ 0

Course 5

• blackboard copy
• course notes pages 86-90

Course 6

• blackboard copy
• course notes pages 91-92, 95-99
• course notes on proof nets pages 1-7
• Homework:
  1. Give the rules of LJ (sequent calculus for intuitionistic logic) with connectives: implication, conjunction, disjunction only.
  2. Define ILL (sequent calculus for intuitionistic linear logic) with connectives: linear implication, tensor, with, plus, of course.
  3. Define Girard's translation (_)^• from LJ (as above) to ILL (as above)
     1. formulas
     2. sequents
     3. rules
  4. Prove that "!Γ^• ⊢ A^•" in ILL implies "Γ ⊢ A" in LJ.
  5. Prove that "Γ ⊢ A" in ILL implies "⊢ Γ^⊥, A" in LL.
  6. Conclude that "Γ ⊢ A" in LJ if and only if "⊢ ?(Γ^•)^⊥, A^•" in LL.

Course 7

• blackboard copy
• course notes on proof nets pages 7-13, 15-22
• course notes pages 103-104, 106-112

Course 8

• preparatory material
• blackboard copy
• additional course notes pages 134-138