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 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).
\nFeel 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 \nFor 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
URL:/NewsandEvents/Archives/2015/newsitem/6858/24- April-2015-Cool-Logic-Daniil-Frumin-ILLC- END:VEVENT END:VCALENDAR