Extracting a certified OCaml library from Coq. 

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

• Timothy Griffin (University of Cambridge), Mukesh Tiwari (University of Cambridge)
• Tuesday 05 July 2022, 13:30-14:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

Abstract:  We present a case study of using Coq to develop  a certified Ocaml library that implements a collection of algebraic  combinators for constructing path algebras. In OCaml, each algebra is a record containing the implementation of algebraic operators  together with certificates attesting to their algebraic properties.    This is joint work with Mukesh Tiwari (University of Cambridge) 

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.