Dove e quando

Is my program correct? This is (or at least should be) the question every programmer ask herself each time she writes a program, and, indeed, this question is really frustrating, since ensuring correctness of programs is a very difficult task. Fortunately, there are several techniques and tools to increase the confidence in the correctness of programs: static and runtime verification, testing and type systems are only some of them. In this talk, we will focus on types, which combine strong formal guarantees with a natural support in programming languages. We will give an overview of a range of type systems with increasing capabilities, coming to discuss the deep connection between types and logic, at the basis of proof assistants. Short bio: Francesco is a second year PhD student in Computer Science. He works with Professors Davide Ancona and Elena Zucca and his research focuses on foundations of programming language semantics. More precisely, he is currently investigating meta-theoretic aspects of operational semantics and coinductive techniques to reason about non-terminating programs. Luca is a third year PhD student in Computer Science, under the supervision of Prof. Davide Ancona. In his research he studies runtime verification and its applications to JavaScript and Node.js, He is currently working on a new specification language called RML (Runtime Monitoring Language).

Contatti