An Introduction to Proof Equivalence

Teachers: Matteo Acclavio and Paolo Pistone

Classes are evey morning from 11h to 13h

Online resurces:

Course schedule

Day 1, 7 August: Overview and Motivations

In this class we discuss the notion of proof and how they can be formalized. After underlying the importance of defining a notion of proof equivalence, we provide the two main approaches to this problem we will explore during the course. We recall the definition of proof system by Cook-Reckhow and the sequent calculi and natural deduction systems for both classical and intuitionistic logic. We then analyze the standard rules permutations we can perform on sequent calculus derivations.

Slides and Notes


Day 2, 8 August: The Paradise of Syllogism and the Forbidden Fruit

We show the Multiplicative Linear Logic and how we can represent proofs using proof nets. We show their canonicity w.r.t. sequent calculus derivations. We show then show that as soon as units or structural behaviors are included in a system, then canonicity may become impossible to achieve.



Day 3, 9 August: Normalization LJ and Denotationional Semantics

Notes Part 1

Slides Part 2


We show the canonicity of disjuntion-free fragment natural deduction with respect normalization and generality. Moreover, in presence of disjunction we can make obtain canonicity with respect to normalization but not with respect to generality. We then define the notion of denotational semantics. We show how a denotational semantics can be easily defined in term of quotient, we show how Game Semantics provides a concrete model for such a semantics.

Day 4, 10 August: Overview



We show the impossibility of having a non-trivial denotational semantics for classical logic by presenting Lafont critical pairs and Joyal's argument. We then present some refinement of sequent calculi allowing to reintroduce canonicity by reducing the non-determinism in proof search. We conclude by introducing the syntax of combinatorial proofs for classical logic, a graphical syntax suitable to provide a canonical representation of proofs. We discuss which rule permutations are captured by this syntax and we discuss the extension of this syntax to other logic.

Day 5, 11 August: Overview

We introduce first and second order quantifiers, and the calculi for first and second order classical and intuitionistic logic. We show the additional challenges in proof equivalence for these logics, and the partial results in the literature. We conclude the course by illustrating applications of proof equivalence to verification, interoperability of theorem provers and suggests the current trends in proof theoretical approaches to programming language theory.



Security 2

Courses classes are Thursday form 9h45 to 11h15 online (the link is available on the moodle)

Online resurces


Course schedule

Week 1, 18 February: Overview

Suggested reading:

What Is Security Engineering

Week 2, 25 February: Attack Trees

Suggested reading:

Week 3, 4 March: free meal case study

Week 4, 11 March: Students presentations

During this class students will give short presentations of some attack trees they produce. Each presentation must include

Suggested reading

Week 5, 15 March (Matteo): Control Access Models

Bell LaPadula Model (MAC)

[The model preserves confidentiality but not integrity of data!]

State of a system

Suggested reading

Week 6, 22 March (Matteo): Chinese Wall

Chinese Wall or Brewer-Nash (DAC + Mandatory access)

Suggested reading

Week 7, 1 April (Ross Horne): Hardware security:

Spring break (week of the 5th of April)

Spring break

Week 8, 15 April (Sjouke Mauw): Intro to protocols

Week 9, 22 April (Ross Horne): students presentations on access control models

Week 10, 29 April (Sergiu Bursuc): Protocol verification inProverif

Week 11, 6 May (Semyon Yurkov): ePayment protocol proof in Proverif

Week 12, 13 May (Reynaldo Gil Pons): Mafia fraud proof in Proverif

Week 13, 20 May (Sergiu Bursuc): Advanced

Week 14, 27 May (Sergiu Bursuc): Advanced

CS2040 - Spring course 2020

Courses classes are on Monday, Wednesday and Thursday form 1h45 to 3h05 in room PL-5 (2bis, Passage Landrieu).


INTRODUCTION TO. JAVA. PROGRAMMING (10th Edition) by Daniel Jiang

Tutor: Gavin Goerke

Online resurces


Base 2 integer conversion

From base 10 to base 2 and

Linear Feedback Shift Register

The "De Brujin" magic trick

!! their card encoding may not corresponds to the one proposed in this exercise!!


Exceptions have to be excaptional!
Some in-depth articles on When and How to use or avoid exceptions:


If you have problems with JavaFX and eclipse on your laptop (like me), you can download IntelliJ (community version) and follow these instructions;

Program of the course

Date Content Assignments
Week 1:
Gen 13
  • Introduction to the course and the course Web site
  • Peergrade
  • Compilers and IDE
  • Introduction Slides
!! Class only on Monday 13 !!
  • Ex1 Part1
  • try Part 2
Week 2:
Gen 20 at 13h45
Gen 23 at 13h45 and at 15h20
  • Data type
  • Program type
  • Type casting
  • An elementary encryption method: Caesar cipher
  • Encrypting via LFSR
No class on Wednesday 22, double class on Thursday 23
  • Write a Caesar cipher encripting program
  • Finish Ex1 and upload the solution on peergrade.
  • Revise course CS1040 topics: Chapters 1-8 of the book (see also myProgrammingLab exercises)
Week 3:
Gen 27 at 13h45
Gen 29 at 13h45
Gen 30 at 13h45 and at 15h20
Objects and Classes
  • What is a class?
  • Unified Modeling Language
  • this
  • What is an object?
  • Differences between objects and classes
  • Why to use OOP?
  • Programming paradigms (procedural vs OOP)
  • here our zoo classes
! Double class on Thursday 30 !
  • Book chapter 9
  • Give feedback to at least 2 peergrade submissions
  • myProgrammingLab exercises on book chapter 9 (at least the two projects at the end of the chapter)
Week 4
Feb 3 at 13:55
Feb 5 at 13:45
Feb 6 at 13:45
OOP thinking & Inheritance & Abstract Classes
  • Why to use OOP?
  • Data access
  • Association
  • Subclasses
  • Inheritance
  • super
  • Override VS Overload
  • Polymorphism
  • here our new zoo
  • ArrayList
  • Excercise: social network (the code we wrote in class)
  • Book chapter 10 & 11 & 13
  • myProgrammingLab exercises on chapter 10
  • myProgrammingLab projects of chapter 11
Week 5
Feb 10 at 13:55
Feb 12 at 13:45
Feb 13 at 13:45
  • Some exercises on the point of the plane (solution w.i.p.)
  • Solution of assignement 2
  • Assignement 2
  • Revise Book chapters 9-11 & 13
  • myProgrammingLab exercises on chapter 10
  • myProgrammingLab projects of chapter 11
17.2 - 28.2 Spring Break
Revise Chapters form 1 to 11 and 13, focussing on 9-11 and 13.
Pay attention to the following key concept summarized in the Chapters Summary (at the end of each Chapter):
  • Chapter 2: 9-12, 17;
  • Chapter 3: 1, 4-6;
  • Chapter 4: 2, 8-11;
  • Chapter 6: all;
  • Chapter 7: 1-9;
  • Chapter 9: all;
  • Chapter 10: 1, 2, 3;
  • Chapter 11: all;
  • Chapter 13: 1-6, 9, 10;
Keep in practice with coding
Week 6
Midterm Exam
  • Theory Test
  • Programming Test
! No class on Wednesday 4 !
Book chapters 1-11 & 13
Week 7
Exception handling and Text I/O
  • exceptions and exception handling
  • Try-Catch
  • File class
  • create/rename/delede files
  • write data to a file
  • read data from a file
  • Excercises
  • ! No class on Monday 9 !
  • Book chapter 12.1-12.11
  • myProgrammingLab exercises on book chapter 12
Week 8
Excercises on File
  • Book chapter 12.10-12.11
  • myProgrammingLab exercises on book chapter 12
Week 9

Scene Builder and Gluon are visual layout tools design GUI.
First steps using scene builder. More details on using scene builder.
With and without scene builder.

  • Book chapter 14, suggested order: from 14.1 to 14.4 -> 14.10 -> from 14.5 to the end
  • First step tutorial: How to create a new windows
  • A more detailed tutorial on JavaFX
  • Send me your final project proposal [What kind of application you want to develop?]
Week 10
Event Driven Programming and some more JavaFX
  • Event source
  • MouseEvent
  • KeyEvent
  • Animations: Animation, PathTransition, FadeTransition, and Timeline
  • Label and Buttons
  • Book chapter 15 untill 16.4
  • HW3 on peergrade
  • Try to make run the boinching ball example a the end of chapter 15
Week 11
JavaFX and I/O
  • Radio Button
  • TextField
  • PasswordField
  • ComboBox and ListView
  • To view and play video and audio
  • Book chapter 15
  • Start to implement the GUI of your final project
  • Try to make this Connection Four look like this.
Week 12
  • Recursion in programming
  • Factorial
  • Fibonacci numbers
  • Fractals
  • book chapters 17 and 18
  • Send me at least a static (does not change by user interaction) but working (that is compiling and showing all the components) graphical interface for your final project before Thursday the 16th.
Week 13
Recursion and Complexity
  • Last project revision
  • Recursion vs Iteration
  • Complexity: O(n) notation
  • What is the complexity of an algorythm?
  • Complexity of sorting algorithms
  • Complexity: 1000000$ Problems
  • Chapter 22-23
  • Send me your first version of the final project before Thursday the 23th
Week 14
class only on Monday: course recap and project revision.
7.5 Final Exam, h12, room: PL-5

Course Syllabus