Formalizing mathematics and critical systems using the Coq proof assistant

Add to your list(s) Download to your calendar using vCal

• Florian Faissole
• Monday 16 July 2018, 15:00-16:00
• Level 9 Seminar Room, EEE Dept..

If you have a question about this talk, please contact George A Constantinides.

Formal methods are techniques used to specify and verify systems, programs or statements using mathematical/logical concepts. There are a wide variety of automated formal methods based on SMT solvers or abstract interpretation. However, these methods are designed in order to verify some particular classes of properties. Proof assistants are software tools designed to help the user to specify systems using a very expressive language and to write proofs about the desired properties of these systems. In this talk, we focus on Coq, a proof assistant based on a rich type system with inductive datatypes. First, we present some significant achievements of Coq in theorem proving and software design. Then, we give a high-level view of the underlying mechanism of Coq, based on the lambda-calculus and the Curry-de Bruijn-Howard correspondance. Finally, we provide a basic demo of Coq to prove logical and arithmetic properties and to formalize the syntax and semantics of a tiny imperative language.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Level 9 Seminar Room, EEE Dept.

Note that ex-directory lists are not shown.