Functional Programming & Proofs


Welcome to you !

This material presents Functional Programming with F# and Proofs with CoqIDE. This one is proposed at the ENSISA, a national school of technical engineers on computer science end technologies.

More precisely, the course starts with functional concepts (e.g. higher-order functions and recursive datatypes) with an application to data processing. Next, it introduces logic of programs and means to specify and proove properties of these programs with the CoqIDE proof assistant and code generator.

START HERE