#5 The History of Coq'Art - Yves Bertot

Type Theory Forall

Контент предоставлен Pedro Abreu. Весь контент подкастов, включая эпизоды, графику и описания подкастов, загружается и предоставляется непосредственно компанией Pedro Abreu или ее партнером по платформе подкастов. Если вы считаете, что кто-то использует вашу работу, защищенную авторским правом, без вашего разрешения, вы можете выполнить процедуру, описанную здесь https://ru.player.fm/legal.

3+ y ago 1:11:46

MP3•Главная эпизода

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:

Yves email: yves.bertot@inria.fr

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

82 эпизодов

#Science #Tech #Pedro Abreu #Type Theory #Academia #Programming Language