Re: Vladimir Voevodsky

["Daniel R. Grayson" <danielrich...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1545 bytes --]

This email from Vladimir seems to be from a time when he had just learned 
more about Coq but had not yet started using it:

From: "Vladimir Voevodsky" <vlad...@ias.edu>
Subject: Re: theorem proving
Date: Wed, December 30, 2009 10:34 am
To: "Daniel R. Grayson" <d...@math.uiuc.edu>

Hi Dan,

thanks for the link. I have heard about this one (from coq-club actually on
which list I am since several years ago). All is well with me, all of the
Bloch-Kato papers are submitted to journals for about a year now and many 
are
accepted. 

I am thinking a lot these days about foundations of math and automated proof
verification. My old idea about a "univalent" homotopy theoretical models of
Martin-Lof type systems survived the verification stage an I am in the
process of writing things up.

I also took a course at the Princeton CS department which was for most part
about Coq and was very impressed both by how much can be proved in it in a
reasonable time and by how many young students attended (45, 35 undergrad +
10 grad!). 

How are you?

Vladimir. 


On Dec 29, 2009, at 8:43 PM, Daniel R. Grayson wrote:

> Volodya,
> 
> This seems to be a good theorem proving conference to attend this summer:
> 
>        https://sympa-roc.inria.fr/wws/arc/coq-club/2009-12/msg00057.html
> 
>                           Call for Papers
>         ITP 2010: Conference on Interactive Theorem Proving
>                 11-14 July 2010, Edinburgh, Scotland
>              http://www.floc-conference.org/ITP-cfp.html
> 
> I hope all is well for you.
> 
> Dan


[-- Attachment #1.2: Type: text/html, Size: 2196 bytes --]