[TYPES/announce] CFP: special issue of JAR on HoTT and univalent foundations

Peter LeFanu Lumsdaine p.l.lumsdaine at gmail.com
Wed Aug 31 08:24:01 EDT 2016

                         CALL FOR PAPERS

                      Journal of Automated Reasoning

Special Issue on Homotopy Type Theory and Univalent Foundations

First Call for Papers

Guest editors:  Peter LeFanu Lumsdaine & Nicolas Tabareau
Submission deadline: 20 Nov 2016
Notification: 20 Mar 2017


This special issue is devoted to the 2nd international workshop on Homotopy
Type Theory / Univalent Foundations (HoTT/UF 2016):


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.

The workshop focus on the practical formalisation of mathematics in
HoTT/UF-based style, in computer proof assistants (Coq, Agda, Lean, …).

Submission to this special issue is open. We expect original articles
(typically 20-30 pages) that present high-quality contributions,
and that must not be simultaneously submitted for publication elsewhere.

Submissions must be written in English and comply with JAR's author


Submission is over easychair:


Please send any queries you may have to Nicolas Tabareau (
nicolas.tabareau at inria.fr)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20160831/228c2da8/attachment.html>

More information about the Types-announce mailing list