<div dir="ltr"><div>Reminder — deadline for contributed talk abstracts is next Wednesday!  Invited talk abstracts now available on the workshop website.<br></div><div><br></div><div>=============================================</div><div>CALL FOR PARTICIPATION</div><div>Workshop on Univalent Foundations and Homotopy Type Theory</div><div>(UF/HoTT, at TLCA 2015)</div><div>=============================================</div><div><br></div><div>-------------------------------------------------------------------------------</div><div><br></div><div>Workshop on Univalent Foundations and Homotopy Type Theory</div><div>29–30 June 2015, Warsaw, Poland</div><div><a href="http://hott-uf.gforge.inria.fr">http://hott-uf.gforge.inria.fr</a></div><div>Co-located with RTA 2015 (RDP/TLCA)</div><div>Abstract submission deadline: 15 April</div><div><br></div><div>-------------------------------------------------------------------------------</div><div><br></div><div>Homotopy Type Theory/Univalent Foundations is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, informed by ideas and tools from abstract homotopy theory.</div><div><br></div><div>One practical goal is the computer formalisation of mathematics in such logical systems.  This workshop aims to focus on that aspect: bringing together researchers on formalisation in HoTT/UF to discuss the various established and experimental proof assistants for it, the different libraries available (HoTT Coq, UniMath, HoTT-Agda…), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.</div><div> </div><div>================</div><div># Invited talks/tutorials:</div><div><br></div><div>* Benedikt Ahrens - Models of type theory in univalent mathematics</div><div>* Thorsten Altenkirch - Univalence for Dummies?</div><div>* Assia Mahboubi - TBA</div><div>* Matthieu Sozeau - Coq support for HoTT</div><div>* Vladimir Voevodsky - From syntax to semantics of dependent types - formalized</div><div><br></div><div>================</div><div># Submissions</div><div><br></div><div>* Abstract submission deadline: 15 April, 2015</div><div><br></div><div>Submissions should consist of a title and abstract, in pdf or text format, via <a href="https://easychair.org/conferences/?conf=hottuf15">https://easychair.org/conferences/?conf=hottuf15</a></div><div><br></div><div>Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.</div><div><br></div><div>=================</div><div># Program committee</div><div><br></div><div>* Benedikt Ahrens (Université Paul Sabatier, Toulouse)</div><div>* Steve Awodey (Carnegie Mellon University)</div><div>* Eric Finster (École Polytechnique)</div><div>* Dan Licata (Wesleyan University)</div><div>* Andrew Polonsky (VU University Amsterdam)</div><div>* Peter LeFanu Lumsdaine (Stockholm University)</div><div>* Nicolas Tabareau (Inria, Rennes)</div><div><br></div><div>=================</div><div># Organisers</div><div><br></div><div>* Nicolas Tabareau (Inria, Rennes)</div><div>* Peter LeFanu Lumsdaine (Stockholm University)</div><div><br></div></div>