BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
BEGIN:VEVENT
UID:/NewsandEvents/Events/Upcoming-Events/newsitem
/6858/24-April-2015-Cool-Logic-Daniil-Frumin-ILLC-
DTSTAMP:20150419T000000
SUMMARY:Cool Logic, Daniil Frumin (ILLC)
ATTENDEE;ROLE=Speaker:Daniil Frumin (ILLC)
DTSTART:20150424T180000
DTEND:20150424T190000
LOCATION:ILLC Seminar Room (F1.15), Science Park 1
07, Amsterdam
DESCRIPTION:In this talk, I will briefly introduce
the theory and practice of Coq - a proof assistan
t based on dependent type theory. A proof assistan
t is a piece of software that provides you with a
semi-interactive environment for constructing and
verifying formal proofs. Coq has been used to prov
e/verify theorems from "pure math" (e.g. odd order
theorem), as well as in software verification (ve
rified C compiler). Feel free to bring your lapto
ps, as the second part of the talk will be a pract
ical hands-on Coq session, during which we will pl
ay a bit with Coq, by defining basic datatypes and
proving simple properties about them. For more i
nformation, see http://www.illc.uva.nl/coollogic/
or contact coollogic.uva at gmail.com
X-ALT-DESC;FMTTYPE=text/html:\n In this
talk, I will briefly introduce the theory and prac
tice of Coq - a proof assistant based on dependen
t type theory. A proof assistant is a\npiece of so
ftware that provides you with a semi-interactive e
nvironment for\nconstructing and verifying formal
proofs. Coq has been used to prove/verify\ntheorem
s from "pure math" (e.g. odd order theor
em), as well as in software\nverification (verifie
d C compiler).

\n Feel free to bring
your laptops, as the second part of the talk will
be a\npractical hands-on Coq session, during which
we will play a bit with Coq,\nby defining basic d
atatypes and proving simple properties about them.

\n \n For more information, see <
a target="_blank" href="http://www.illc.uva.nl/coo
llogic/">http://www.illc.uva.nl/coollogic/ or
contact coollogic.uva at gmail.com

\n
URL:/NewsandEvents/Events/Upcoming-Events/newsitem
/6858/24-April-2015-Cool-Logic-Daniil-Frumin-ILLC-
END:VEVENT
END:VCALENDAR