BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Extracting a certified OCaml library from Coq.  - Timothy Griffin
  (University of Cambridge)\, Mukesh Tiwari (University of Cambridge)
DTSTART:20220705T123000Z
DTEND:20220705T133000Z
UID:TALK175751@talks.cam.ac.uk
DESCRIPTION:Abstract:&nbsp\; We present a case study of using Coq to devel
 op&nbsp\;\na certified Ocaml library that implements a collection of algeb
 raic&nbsp\;\ncombinators for constructing path algebras. In OCaml\, each a
 lgebra\nis a record containing the implementation of algebraic operators&n
 bsp\;\ntogether with certificates attesting to their algebraic properties.
 &nbsp\;\n&nbsp\;\nThis is joint work with&nbsp\;Mukesh Tiwari (University 
 of Cambridge)&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR