The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

=============================================
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 of the programme 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
* Thorsten Altenkirch

* Matthieu Sozeau
* Vladimir Voevodsky

================
# 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)