Periodic Reporting for period 1 - Cameleer (Principles and Methods to Verify OCaml Programs)

Deductive software verification, a subject within the broader field of formal methods, proposes a very ambitious path: to turn the correctness of a computer program into a mathematical statement, and then prove it. This project aims to develop a deductive verification...