University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Extracting a certified OCaml library from Coq. 

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Extracting a certified OCaml library from Coq. 

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Type the title of a new list here Room to be announced Classics Faculty IfM Buns Talk

Other talks

Differences between Robin and Neumann eigenvalues The United States of America at 250: Reflections on the Past, Present and Future of Independence title abstract tbc Loke CTR Annual Meeting 2026 - Epigenetics of embryogenesis and placentation The elephant in the room: Machine Learning directly into physical models Afternoon Break
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity