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/2020/newsitem/11271/1- --4-February-2020-Workshop-Mathematical-Language-P ractical-Type-Theory-Bonn-Germany DTSTAMP:20191103T154523 SUMMARY:Workshop "Mathematical Language & Practica l Type Theory", Bonn, Germany DTSTART;VALUE=DATE:20200201 DTEND;VALUE=DATE:20200204 LOCATION:Bonn, Germany DESCRIPTION:Formal Mathematics aims at the complet e formalization and formal checking of mathematica l statements and proofs. In recent years practical ly efficient computer assisted systems have been d eveloped and used to formally verify outstanding m athematical results. However, formalizations in th e currently dominating systems are written in lang uages that resemble computer code and are neither accessible nor attractive to the wider mathematica l community. The workshop will be looking into way s to overcome this barrier by using (controlled) n atural language input for proof systems. The wor kshop will bring together invited experts from lin guistics, formal mathematics, type theory and the LEAN prover system. After some invited talks on Sa turday we envisage intense interactions of various groups with ample time for discussion and explora tory experiments. Participants will be asked to gi ve brief contributed presentations of their resear ch relevant to the conference topic. The Workshop is able to offer five scholarships for PhD stude nts and new PhDs with previous experience in forma l mathematics. The workshop will cover local costs and give travel support. Apply before November 30 , 2019. X-ALT-DESC;FMTTYPE=text/html:\n
Formal Mathema tics aims at the complete formalization and formal checking of mathematical statements and proofs. I n recent years practically efficient computer assi sted systems have been developed and used to forma lly verify outstanding mathematical results. Howev er, formalizations in the currently dominating sys tems are written in languages that resemble comput er code and are neither accessible nor attractive to the wider mathematical community. The workshop will be looking into ways to overcome this barrier by using (controlled) natural language inpu t for proof systems.
\n\nThe workshop will bring together invited experts from linguistics, formal mathematics, type theory and the LEAN prove r system. After some invited talks on Saturday we envisage intense interactions of various groups wi th ample time for discussion and exploratory exper iments. Participants will be asked to give brief c ontributed presentations of their research relevan t to the conference topic.
\n\nThe Worksho p is able to offer five scholarships for PhD students and new PhDs with previous experience in formal mathematics. The workshop will cover local costs and give travel support. Apply before Novem ber 30, 2019.
URL:https://www.hcm.uni-bonn.de/events/eventpages/ 2020/mathematical-language-practical-type-theory-2 020/ END:VEVENT END:VCALENDAR