From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10247 Path: news.gmane.io!.POSTED.ciao.gmane.io!not-for-mail From: Chris Kapulkin Newsgroups: gmane.science.mathematics.categories Subject: Call for Participation: HoTT/UF 2020 - July 5-7 Date: Thu, 25 Jun 2020 09:17:44 -0400 Message-ID: Reply-To: Chris Kapulkin Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="ciao.gmane.io:159.69.161.202"; logging-data="4323"; mail-complaints-to="usenet@ciao.gmane.io" To: Homotopy Type Theory , categories@mta.ca, HoTT Electronic Seminar Talks Original-X-From: majordomo@rr.mta.ca Thu Jun 25 21:29:36 2020 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.55]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1joXZ2-0000y3-4I for gsmc-categories@m.gmane-mx.org; Thu, 25 Jun 2020 21:29:36 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:58710) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1joXYd-0001rZ-Bf; Thu, 25 Jun 2020 16:29:11 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1joXYa-0003Th-I2 for categories-list@rr.mta.ca; Thu, 25 Jun 2020 16:29:08 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10247 Archived-At: CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations July 5-7, 2020, The Internet https://hott-uf.github.io/2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Registration Registration is free of charge, but required. The details can be found on the event website. # Invited talks * Carlo Angiuli (Carnegie Mellon University) From raw terms to recollement * Liron Cohen (Ben-Gurion University) Building Effectful Realizability Models, Uniformly * Pierre-Louis Curien (Universit=C3=A9 de Paris) A syntactic approach to opetopes, opetopic sets and opetopic categories # Contributed talks 21 talks were accepted by the Program Committee. Their titles and abstracts are available on the event website. # Schedule The event will take place from July 5-7, 2020. The talks are scheduled between 2 PM and 7:30 PM CEST (UTC+2). Detailed schedule is now available on the website. # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]