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\n The 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\n The 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