1-4 Feb 2020
Bonn, Germany
The Workshop "Mathematical Language and Practical Type Theory" organized by Thomas Hales (Pittsburgh) and Peter Koepke (Bonn) is able to offer five scholarships for PhD students. The Naproche (Natural Proof Checking) group at Bonn and the Formal Abstracts initiative of Tom Hales are working on a controlled natural language for the LEAN prover system. The upcoming workshop shall promote these efforts by bringing together invited experts from linguistics, formal mathematics, type theory and LEAN, with time for discussions and exploratory hands-on experiments. See the evolving website at https://www.hcm.uni-bonn.de/events/eventpages/2020/mathematical-language-practical-type-theory-2020/ We are able to offer a small scholarship program during the workshop for PhD students and "new" PhDs (less than one year after completion) with previous experience in formal mathematics. Scholars are given the opportunity to obtain first-hand impressions of controlled mathematical languages and their parsing and further processing in formal mathematics systems. The workshop will cover local costs and give travel support. We invite informative applications including CV, research statement and a letter of recommendation to mlaptt(at)hcm.uni-bonn.de before November 30, 2019. Note: Participation in the workshop is by individual invitations. For further information please email koepke(at)math.uni-bonn.de -- [LOGIC] mailing list http://www.dvmlg.de/mailingliste.html Archive: http://www.illc.uva.nl/LogicList/ provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam