This is the homepage of the course on Concurrency Theory, held at the University of Southern Denmark in Fall 2017.

Each week, there are two allocated times for the course (on two separate days). The first one is a frontal lecture. The second one is a joint exercise/reading class for students only.

For each exercise/reading class, there will be a reading assignment (possibly with exercises). You can find these in the section "Reading/Exercise Assignments" at the bottom of this page. You are encouraged to do the reading and exercises together, if you like. You should keep three things in mind while you do it (the general idea is: write everything down!). First, write down your solutions to exercises (if any). Second, write down questions about things that you did not understand. Third, if you come up with new questions that are not mentioned in the lectures or the material, write them down too. Challenges for your colleagues and/or the teacher for the lectures are welcome!

• Course Evaluation

This list is updated throughout the course, so come back to check it out every week!

• Introduction Slides
• Notes on Deductive Inference, by Frank Pfenning: https://www.cs.cmu.edu/~fp/courses/15816-s12/lectures/01-inference.pdf
• Notes on From Rules to Propositions, by Frank Pfenning: https://www.cs.cmu.edu/~fp/courses/15816-s12/lectures/02-propositions.pdf
• Notes from Week 38
• Parrow, Joachim. An Introduction to the Pi-Calculus. https://www.risc.jku.at/education/oldmoodle/file.php/28/intro-1.pdf
• Aceto, Luca, et al. Reactive systems: modelling, specification and verification. Cambridge University Press, 2007. http://rsbook.cs.aau.dk/
• Notes on Choreographies, Part 1
• Notes on Choreographies, Part 2
• Notes on Choreographies, Part 3 [LaTeX source, which uses the proof-dashed package]
• Notes on Choreographies, Part 4
• Notes on Choreographies, Part 5
• Exam examples

For the material that I refer to here, see the list above in section "Material".

• Week 36. In Material 2, read pages 1--6 and do Exercise 3.(i). Try to solve this exercise: consider a theory consisting of the rules "sym", "e", and "trans" from pages 2 and 3; given a proof of some path(x,y) (so that's the conclusion of the proof), how long is this path? Try also this exercise: in the same theory as in the last exercise, consider the graph obtained by adding two nodes e and f to the graph displayed in page 2; assume edge(e,f) (there is an edge between e and f), but otherwise e and f are not connected to any other nodes; can you demonstrate that path(a,f) *cannot* be proven? Discuss your solution with your colleagues.
• Week 37. Refresh your memory on ephemeral truth by re-reading Section 3 of Material 2. Read Sections 4 and 5 of Material 2. Read Sections from 1 to 5 of Material 3. Read Section 8 of Material 3, but ignore the parts about identity expansion and cut reduction (these are for the next lecture).
  Prove that ⊦ A -o A.
  Prove that ⊦ (A ⊗ B) -o (B ⊗ A).
  Prove that ⊦ (A ⊗ (A -o B)) -o B.
• Weeks 38-41. Read and do the exercises in Material 4.
• Week 43. Read Sections 2 and 5.4 from Material 5, Section 2.2.3 from Material 6 and do exercises 2.8, 2.11, 2.12 from Material 6.
• Week 44. Read and do the exercises in Material 7.
• Week 45. Read and do the exercises in Material 8.
• Week 46. Read and do the exercises in Material 9.
• Week 47. Read and do the exercises in Material 10.
• Week 48. Read and do the exercises in Material 11.
• Week 50. Exercises 3.3, 3.4, 3.5, 3.11, 3.19, 3.25 in Material 6.