ISR 2024 – Track B

Schedule

	Monday	Tuesday	Wednesday	Thursday	Friday	Saturday
9:00 – 10:30	1	4	7	excursions	e4	12
10:30 – 11:00	break				break
11:00 – 12:30	2	5	e3		10	13
12:30 – 14:00	lunch				lunch
14:00 – 15:30	3	e2	8		11	e6
15:30 – 16:00	break				break
16:00 – 17:30	e1	6	9		e5	test

Monday

• lecture 1: introduction, syntax and opertional semantics of untyped lambda calculus
  
• lecture 2: simple type theory, formulas-as-types and proofs-as-terms
  
• lecture 3: first-order dependent type theory, formulas-as-types and proofs-as-terms
  
• exercises 1
  

Tuesday

• lecture 4: Coq: predicate logic, interactive theorem proving using tactics
  
• lecture 5: Coq: inductive types
  
• exercises 2
  
• lecture 6: polymorphic types
  

Wednesday

• lecture 7: calculus of constructions and the type theory of Coq
  
• exercises 3
  
• lecture 8: simple meta theory of type systems and type checking algorithm
  
• lecture 9: Church-Rosser property
  

Friday

• exercises 4
  
• lecture 10: weak normalization and strong normalization property
  
• lecture 11: normalization by evaluation
  
• exercises 5
  

Saturday

• lecture 12: a functional programmer's view on type theory
  
• lecture 13: homotopy type theory
  
• exercises 6
  
• test
  

Course Link

link