BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2015/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;TZID=Europe/Amsterdam:20150424T180000
DTEND;TZID=Europe/Amsterdam: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 https://www.illc.uva.nl/coollogic/
  or contact coollogic.uva at gmail.com
X-ALT-DESC;FMTTYPE=text/html:\n        <p>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 &quot;pure math&quot; (e.g. odd order theor
 em), as well as in software\nverification (verifie
 d C compiler).</p>\n        <p>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.
 </p>\n    \n        <p>For more information, see <
 a target="_blank" href="https://www.illc.uva.nl/co
 ollogic/">https://www.illc.uva.nl/coollogic/</a> o
 r contact <a class="email">coollogic.uva <span cla
 ss="at">at</span> gmail.com</a></p>\n    
URL:/NewsandEvents/Archives/2015/newsitem/6858/24-
 April-2015-Cool-Logic-Daniil-Frumin-ILLC-
END:VEVENT
END:VCALENDAR