#5 The History of Coq'Art - Yves Bertot
Type Theory Forall
In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept.
Links:
Affichage et manipulation interactive de formules mathématiques dans les documents structurés - Check figure 15 for an example on how Yves’ tools would build trees internally
A video showing his tool in practice, doing proofs with mouse clicks
A Genereic Approach to Building User Interfaces for Theorem Provers
Next Episodes
#4 Theorem Provers, Functional Programming and Companies - Eric Bond @ Type Theory Forall
📆 2021-02-15 05:00 / ⌛ 01:14:22
#3 ML for PL and Mental Health - Dan Zheng @ Type Theory Forall
📆 2021-02-01 05:00 / ⌛ 01:08:01
#2 Grad School Life - Rajan Walia and John Sarracino @ Type Theory Forall
📆 2021-01-10 05:00 / ⌛ 00:57:55
#1 What is PL research? - Prof. Ben Delaware @ Type Theory Forall
📆 2020-12-23 05:00 / ⌛ 00:57:55
#0 Cool Internships in PL - Believe or not there are quite a few companies interested in Programming Languages Research. @ Type Theory Forall
📆 2020-12-14 05:00 / ⌛ 00:31:59