2018 Verified programming and type theory

Organisation

The lectures will take place
Thursdays: 10:00 -- 12:00.
Calle Montalegre 6 in a room yet to be decided upon. The start date is Thursday, March 1.

The organizers of the course are Ana Borges, Joost J. Joosten, Aleix Solé Sánchez and Eric Sancho.

The course is part of the apprenticeship project of the UB and as such the students will have to develop notes that can be used for future hires of the company. This project constitutes for 6 European Credits so that the students are to dedicate 120 hours to it. We decided to spread this of 12 weeks of 10 hours dedication per week. Apart from taking notes and learning the material and challenging the lecturers, there are several other more commercial tasks that are performed by the students.
Week 1 | | Week 5 | | Week 9
Week 2 | | Week 6 | | Week 10
Week 3 | | Week 7 | | Week 11
Week 4 | | Week 8 | | Week 12

Week 1

(Feb 26 -- Mar 2)

Our first lecture.

Martí Grau:

The lecture began with an introduction by Joost on the aim of the company and the reverse engineering nature of software verification. It was briefly mentioned that the process involves finding a proof in intuitionistic logic, which will correspond to a program. Then Ana spoke about getting witnesses in intuitionistic proofs, and how some equivalences in classical logic don't hold in intuitionistic logic, such as ∃ α ≢ ¬ ∀ ¬ α. The course will first deal with inductive definitions and recursion. Thus, we began trying to come up with some examples of inductive definitions, namely for the natural numbers (or "aliens"), their addition, their product, their factorial function and the function of "being less than".

Week 2

(Mar 5 -- 9) "Macho Muerto, abono pa mi huerto" on the wall, strike, piquetes and other aggressions prevented us from having class.

Week 3

(Mar 12 -- 16)

Having given examples of inductive definitions and recursive functions in the last class, this week we have re-written them in OCaml language. We have started to learn the basics of OCaml programming, its syntax and how to define types and recursive functions and its difference with other programming languages. We have written in OCaml the type "natural number" (or aliens) and "list" (or queue) and the recursive functions of the sum and product of natural numbers, the length and total of a list (that returns the number of elements of a list and its sum, respectively) and the functions below_n, map and <t.

Week 4

(Mar 19 -- 23)

Week 5

(Mar 26 -- 30)

Martí Arnau:

In the last class, which was led by Joost, we briefly reviewed the goals recently set in the quarterly business meeting: 1) to come up with both a Driver's List and an Activity List from the Tachograph's data and 2) to develop an Events List and a list of Finable Objects.

Then we touched upon the notion of types and their ability to specify the kinds of entities we work with. We saw that type checking, i.e. the automatic procedure through which OCaml infers the type of a certain term, is done by means of a derivation. For example, we wrote the derivation needed to establish that A(O, A(O, E) is of type queue.

Finally, we corrected a coupe of exercises that we had trouble with: [elim] and [range]. We recursively defined and used an abbreviation of queue to write queues more easily in the following way:

[ ] := E
[a, x0, ... , xn] := A(a, [x0, ... , xn])

When solving [range] we realized that, if carefully read, the statement has some ambiguities (Joost pointed out that this process of finding ambiguities and deciding how to interpret them is very common when formalizing the law):

The solution we devised for [range] (and was or wasn't it the one Ana had thought of?) was the following:

let rec range l r =
match r with
I O -> if eq l O
then [O]
else E
I Sd -> if lt Sd l
then E
else if eq l Sd
then Sd
else [range l d, Sd];;

Week 6

(Apr 2 -- 6)

Alba Porras: The 5/4/18 class we saw the main types of Ocaml programming language and also its basic syntax. Ana taught us to implement basic functions such as addition. We also talk about the syntax of lists and polymorphic variables. Finally we saw lists in which the type of variable of its elements is not specified.

Week 7

(Apr 9 -- 13)

Gina Tarrach: In today's class we have talked about different aspects of OCaml's programming language. Firstly, we have learned how to specify the type of the inputs and the output of a function, instead of letting OCaml figure it out. We have then talked about local and global identifiers, its differences and when and how to use local ones. Lastly, we have introduced (and put into practice) another type of recursion: tail recursion, which is more efficient and less memory and time consuming than the "standard" one. 

Week 8

(Apr 23 -- 27)

Alba Porras: The class began with a review of propositional logic. We saw an inductive definition of the formulas.
Then we started to learn how to encode the propositional logic in Ocaml:
First, we defined the type 'variable'.
Second, we defined the type 'formula' like this:
type formula =
(*basic cases: *)
|var of variable (*an object of type variable*)
|Bot (*falsum*)
(*inductive cases: *)
|Neg of formula (*for the negation *)
|And of formula * formula (* for the conjunction*);;
Thus, a phi formula can give us an output such as: And (Bot, Neg Bot);;
As this way of defining the formulas can be difficult to read, we defined the functions string_of_variable and string_of_formula to use symbols more similar to those of the propositional logic.
Finally, we define the function is_tauto that given a formula, outputs a bool: true if the input formula is a tautology and false if it is not.

We also discussed modules and how to organise your code when programming with OCaml (and more generally, with any other language). By creating modules (and its respective interfaces), programming becomes more systematic and it is easier to work with other colleagues: each one works in a different module and doesn't interfere with the code of the other. Besides, having different modules helps you categorize the functions you implement: for example, all functions related to variables go to the module 'Variables', all functions related to formulas go to the module 'Formulas', etc. In this class we have learned how to do that in OCaml, what are the characteristic of the module files (.ml) and the interface files (.mli) and how to compile them. 

Week 9

(Apr 30 -- May 4)

Today we talked about sorting algorithms. We used cards to simulate several different sorting methods, and we wrote down the steps taken. We learned about insertion sort, quicksort, merge sort and bubble sort, and mentioned some others.

Week 10

(May 7 -- 11)

On the 10/05 we had the meeting with Guillermo. The companions explained the work they had done so far. After a pause, Gina, Martí and I explained to Guillermo what our practices consist of. Finally, Juan presented the idea of his master's tesis.

Week 11

(May 14 -- 18)

Today we talked about trees, specifically binary search trees. We saw how to implement them (and operations on them) in OCaml, and why they are useful for searching.

Week 12

(May 21 -- May 25) Another strike on the 24th of May. Therefore we didn't have a class.

Week 13

(May 28 -- June 1)

Today was the last class. We spent it finishing our homework with Ana's help, who gave us advice in some of the exercises we hadn't been able to do. Once finished, we did some of the exercites listed in the website https://ocaml.org/learn/tutorials/99problems.html . At last, we shared our impressions and opinions on this period of 'pràctiques' and we all agreed that it had been a very good, interesting and useful opportunity for us to learn the OCaml language and the work of Formal Vindications.