Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
De Christoph Koutschan
Creative telescoping for D-finite functions - Lecture 2
De Christoph Koutschan
Apparaît dans la collection : 2014 - T2 - Semantics of proofs and certified mathematics
The programming language Mezzo is a member of the ML family, from whom it inherits algebraic data types, first-class functions, and automatic memory management. It is equipped with a rich type system that controls aliasing and access to mutable memory. This static discipline rules out certain programming mistakes, guarantees data race freedom, and opens up some new possibilities, such as gradual initialization and type(state) changes. In the first lecture, I will present Mezzo via a series of examples. In the second lecture, I would like to present the meta-theory of Mezzo. It is organized in a modular manner and has been machine-checked in Coq.