From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 12 Oct 2017 12:06:20 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: <69c716dc-7fbf-4c07-a128-21c75fc996da@googlegroups.com> In-Reply-To: References: Subject: Re: Vladimir Voevodsky MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_15846_840656321.1507835180569" ------=_Part_15846_840656321.1507835180569 Content-Type: multipart/alternative; boundary="----=_Part_15847_1342653996.1507835180570" ------=_Part_15847_1342653996.1507835180570 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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" Subject: Re: theorem proving Date: Wed, December 30, 2009 10:34 am To: "Daniel R. Grayson" 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 ------=_Part_15847_1342653996.1507835180570 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
This email from Vladimir seems to be from a time when he h= ad just learned more about Coq but had not yet started using it:

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

Hi Dan,

thanks for t= he link. I have heard about this one (from coq-club actually on
w= hich 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 an= d many are
accepted.=C2=A0

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

I also took a course at the Princeton CS department which was for mo= st 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!).=C2=A0

How are you?

Vladimir.=C2=A0

<= /div>

On Dec 29, 2009, at 8:43 PM, Daniel R. Grayson wro= te:

> Volodya,
>=C2=A0
&= gt; This seems to be a good theorem proving conference to attend this summe= r:
>=C2=A0
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 https://s= ympa-roc.inria.fr/wws/arc/coq-club/2009-12/msg00057.html
>=C2= =A0
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Call for Papers
>=C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0ITP 2010: Conference on Interactive Theorem = Proving
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A011-14 July 2010, Edinburgh, Scotland
>=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 http://www.floc-conference.org/ITP-cfp.h= tml
>=C2=A0
> I hope all is well for you.
>=C2=A0
> Dan

------=_Part_15847_1342653996.1507835180570-- ------=_Part_15846_840656321.1507835180569--