Thursday 1 March 2018, 14:00, LSV: An introduction to certified programming using Agda, Mathieu Montin (IRIT).

Agda is a proof assistant based on the type theory. More precisely, it provides a programming language akin to certified programming combined with interactive tools to help building programs and associated proofs. This language is dependently typed, which means it allows the expression of properties both on data types and functions. The development tool is an Emacs mode which allows the user to interact with several underlying features, including - but not limited to - the automated proof helper, the interpreter or the unifier. Agda indeed embeds a unifier which allows for instance to unify the operands of equality proofs, hence easing the handling of such proofs. This talk relies an example of refinement between automata accepting numbered sequences of events to introduce this development environment. This refinement heavily relies on the mechanization of the Euclidean decomposition over natural numbers. It provides explanations about the basic features of Agda as well as examples of more advanced possibilities, such as helping the termination checker by providing a convenient data type, or helping the unifier when dealing with non- decidable properties relying on injectivity proofs.