HoTT/UF workshop at TLCA Warsaw, abstract deadline Apr 15

[Peter LeFanu Lumsdaine]

Reminder — deadline for contributed talk abstracts is next Wednesday!  Invited talk abstracts now available on the workshop website.

=============================================

CALL FOR PARTICIPATION

Workshop on Univalent Foundations and Homotopy Type Theory

(UF/HoTT, at TLCA 2015)

=============================================

-------------------------------------------------------------------------------

Workshop on Univalent Foundations and Homotopy Type Theory

29–30 June 2015, Warsaw, Poland

http://hott-uf.gforge.inria.fr

Co-located with RTA 2015 (RDP/TLCA)

Abstract submission deadline: 15 April

-------------------------------------------------------------------------------

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.

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.

 

================

# Invited talks/tutorials:

* Benedikt Ahrens - Models of type theory in univalent mathematics

* Thorsten Altenkirch - Univalence for Dummies?

* Assia Mahboubi - TBA

* Matthieu Sozeau - Coq support for HoTT

* Vladimir Voevodsky - From syntax to semantics of dependent types - formalized

================

# Submissions

* Abstract submission deadline: 15 April, 2015

Submissions should consist of a title and abstract, in pdf or text format, via https://easychair.org/conferences/?conf=hottuf15

Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.

=================

# Program committee

* Benedikt Ahrens (Université Paul Sabatier, Toulouse)

* Steve Awodey (Carnegie Mellon University)

* Eric Finster (École Polytechnique)

* Dan Licata (Wesleyan University)

* Andrew Polonsky (VU University Amsterdam)

* Peter LeFanu Lumsdaine (Stockholm University)

* Nicolas Tabareau (Inria, Rennes)

=================

# Organisers

* Nicolas Tabareau (Inria, Rennes)

* Peter LeFanu Lumsdaine (Stockholm University)