From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 9335 invoked from network); 19 Dec 2023 02:42:49 -0000 Received: from mail-qv1-xf3b.google.com (2607:f8b0:4864:20::f3b) by inbox.vuxu.org with ESMTPUTF8; 19 Dec 2023 02:42:49 -0000 Received: by mail-qv1-xf3b.google.com with SMTP id 6a1803df08f44-67f3275e14fsf38583966d6.1 for ; Mon, 18 Dec 2023 18:42:49 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1702953768; cv=pass; d=google.com; s=arc-20160816; b=x8ft8zfSj36C6GABRMwC2hI5SnD4jcVfYQ/6Ysjdh+cNlt3jtojRhG/ocwdjGMXh/j 1OHPypbTw/Is2OcUnbdf1SovCcXHiUU6YUl7Uyt+ZRz5VmjyGbM0vMSnkb04LMjBJnNW ZGbbencP6T8yYGGoe3NJDteTT1HPotv3tm6iHV4YUn+0D2sXSTPwTpzmXjskkjQufMwf ZzAEygTCoE8MaltkYjUDYyHifse7aF22st2LitLdWrKWjszOXbkXf+KKSGujnVX0Z3Vb dGfjXJYurl7aXPW+jPsQl+K43PnwLHZYCEPVMXg6aPwLRmdMx6dznW9IWDqs8jUS1qys VFyw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=FkBQTcaq8V7FJAPnTNn1QbxAmG8kRKs/UOQReLsa3nw=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=KrphKmlyf2svVTiPNkbna1Ns+aPa0Vgg+Vkbe6i8BwX07EdYR8TtSZcRLWUuqnhdZa C78XJdTpmotKNlzf2a4/eMtCBM+NpxS+7/QuorUCM02Ay0P+sAB/QtjzZhZV7axcQOG6 QR9NycbXX+HdFqy6esfrVvN5fvYL811ICl+kvYuzLi7AZRKwadRZzxiFzMfl7oVVivwP rZ+4Xeb9K5Teh9hMjYLEYEUF6tXpz4MEZ0iM0ehy5sDV1uJOev3BRWbg6izRP1KZR4tN YiyRi9Y+fD8H09vvzJoAqUGfRppNvNwbPL97swjxji96NDPgbuJ3zS4dX4gq9YMSSEgy eYrw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=iacKGl0G; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::233 as permitted sender) smtp.mailfrom=weinbergerjonathan@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1702953768; x=1703558568; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=FkBQTcaq8V7FJAPnTNn1QbxAmG8kRKs/UOQReLsa3nw=; b=XTt3nFCWGAYFhqRitwlFBeg6s5I13cWK+NjeyNMeG/P7Nf1ggtQHjNnAgxsjYKlKBO JERFByS7bsxHWMr7PwXW3Vf3tZKrJi67NNBK8yxT7kLYTItmtEKynEr+uh4ezsqlqT/c hZzVwpkfdpZRD+xrpizG0MVYfuBLy6IOO3HwgO5RKnLhC90W3JVpH8h3rhpF/zX3Efku +w6ZyvM/j83BcC/daoO3DgZ5HxQx4IYj30U+NT++Hp6t990X85xStmlKxtAug1Zeujc9 HyYYyANmH2DjIIXDSxlhSFlyvVijCj659TCqRh4urlNNxvtUUx+dRVrX8PLSziw1mo9m s74w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1702953768; x=1703558568; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=FkBQTcaq8V7FJAPnTNn1QbxAmG8kRKs/UOQReLsa3nw=; b=WFJtsRqVCCo6OH7aqjEb7VEeG1Je/Fa6qNKnwEry/xsS+Zu7h/Dd4IVVv03x9t89lY W0NfB+jdt5CmrXHiiFwBrw2Mw5R2tFcLO12rG756RBIHxpRLPKJD0ioXjlIUau9z4y4r QZlPPwaVJ7TEhJ0RbzoYxStTkx4Vhgr/+a74CwUxEdr4mTnCiglxftUs9NtCOTCtgKXu nItx7woxOB7BlGncjfTBJzgpWPOTO8IrUqPszkAuKwBvanSbUkgU6H1sXoRs/vQXtLrr zjBQjui7PoEb9o6VQm8l0w68kqH7uqJN6KxrhCOgwQjoZAtW/lrgElj/o+yJDdADj4XJ HWJg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1702953768; x=1703558568; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:mime-version:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=FkBQTcaq8V7FJAPnTNn1QbxAmG8kRKs/UOQReLsa3nw=; b=S9UDSLB22qQypdVoSlM9y0M2AMGrk8FDwmsNY817eehJkwHnCTEfDR/nRNsbO2+B8x TvEFR8jzIuGwd2LpWsrOKRtma29Q76bB/SesjmdAjpqce+RfqG2qs8eoJfAoX4yJz2SI nayIUr7XqW3YArEWStoS/LLOXd1Uzm01XbEV5s15OvAnaGDMlFCJn27eCz7qQ8hSHZjo g4rn7h/CS/O++DswsoQUNu8MzSYwHC+5+4M5Wmv3W2n8//7nLFHEZ/EfAWuj9eQ04Hhm svkAxyx7kHF9NfVLM7CQKN3xTUkmQ4Hj7GYEoGJslWjV6NBtYp5rmMB919PqNncGZSm1 a0vw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOJu0YxC6VowzwXc/5uS5aQD6xY5iu+1ipY28gjAIpDqjbfTdyrCo/w8 0eo6ELQ/3ONHHRVlVwmhNLY= X-Google-Smtp-Source: AGHT+IE6XT4LPusn+bk9WeLBGRdjv34uce0I0ifjf4y2CkBnLzNAzc4fA/HFFI0nwqNSI1VfwwzT7A== X-Received: by 2002:a05:6214:2583:b0:67a:a721:e144 with SMTP id fq3-20020a056214258300b0067aa721e144mr26363332qvb.113.1702953767536; Mon, 18 Dec 2023 18:42:47 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6214:d4d:b0:67a:9611:38ee with SMTP id 13-20020a0562140d4d00b0067a961138eels2735147qvr.2.-pod-prod-07-us; Mon, 18 Dec 2023 18:42:46 -0800 (PST) X-Received: by 2002:ad4:5ca4:0:b0:67f:5077:e1fe with SMTP id q4-20020ad45ca4000000b0067f5077e1femr2497410qvh.70.1702953765948; Mon, 18 Dec 2023 18:42:45 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1702953765; cv=none; d=google.com; s=arc-20160816; b=scN+1ydCro+PpLTonJ4UGqXzboWYxj8GXhnhDHo0WBy5X7x3wSaZgI0HJTrap17xLM J/dKF7ewV7OKO84tbgvzFfKLJRZdEMR1FHjcaGDwCeKtsim7eX28lBjaONdTi2Q3yOPE dD7LsbSInG7+OcCdUfZgKgrWV2PLdQwOMSAFJM3lknSl8VpbfUpbLQqTIGIbMCeADLjZ 8q1IYW3KceZknXUNwy1fnyF4mzFZF8p1C00V9DTHewV9V3gzhig41QCXrA3dyG150akX FkG2JdzvgvzKS4mUMunNnELpRHszOXw7XEBd/616l2mxux48wwacRwp5HX7UdndQEqIs kKLQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=ffOvEqaonnouVRhek82lTIvU/CPBnOYHl0jgpmlByIg=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=yDI0hc4XkMg0LhWeOB+ij0mtSzs6mqrsxbrX66m1gxRqpzaJ8JM2Yjdjsyw62tGqK1 DqF93adysUDCEkLmroeqXGQDRE6mGN5wqobrNJ0c0Ta3daUUeNkgmftcIuKN2Px/Uwoe TaCcg+QmuaKq7606bnJyjNthouYTLfep4RPzT6X0YF/+wZPiQa30ixImuLMdyk58SYsw sv+8N/I/QwCnLNY2Nk1dtfBz6JzGzRU9avtd2z5F2TsDfoT2eHiMbj37nX6MJf/6lq35 9OcRVJqKno1N2JeAxXZ8JZYNxmV6Mg6dWygKPvEVB3hqbh7JNEzXjwsnuYJiG/ZqL21c xVZA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=iacKGl0G; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::233 as permitted sender) smtp.mailfrom=weinbergerjonathan@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x233.google.com (mail-oi1-x233.google.com. [2607:f8b0:4864:20::233]) by gmr-mx.google.com with ESMTPS id fv6-20020a056214240600b0067a9e5ac0c4si594195qvb.8.2023.12.18.18.42.45 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 18 Dec 2023 18:42:45 -0800 (PST) Received-SPF: pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::233 as permitted sender) client-ip=2607:f8b0:4864:20::233; Received: by mail-oi1-x233.google.com with SMTP id 5614622812f47-3ba00fe4e94so3197924b6e.1 for ; Mon, 18 Dec 2023 18:42:45 -0800 (PST) X-Received: by 2002:a05:6808:1290:b0:3b8:9b7f:40e8 with SMTP id a16-20020a056808129000b003b89b7f40e8mr23859237oiw.17.1702953765267; Mon, 18 Dec 2023 18:42:45 -0800 (PST) MIME-Version: 1.0 From: Jonathan Weinberger Date: Mon, 18 Dec 2023 21:42:34 -0500 Message-ID: Subject: [HoTT] HoTT/UF 2024: First Call for Contributions and Participation To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000003f6edd060cd3d2e1" X-Original-Sender: weinbergerjonathan@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=iacKGl0G; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::233 as permitted sender) smtp.mailfrom=weinbergerjonathan@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --0000000000003f6edd060cd3d2e1 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D 2ND CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2024, co-located with WG6 meeting of the EuroProofNet COST action) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations April 2 - 3, 2024, Leuven, Belgium https://hott-uf.github.io/2024/ Co-located with the WG6 meeting of the EuroProofNet COST action April 4 - 5, 2024 https://europroofnet.github.io/wg6-leuven/ ------------------------------------------------------------------------ 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person with support for remote participation. We encourage online participation for those who do not wish to or cannot travel. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Invited speakers * Rafa=C3=ABl Bocquet (E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Hungary) * Matthias Hutzler (University of Gothenburg, Sweden) * TBA =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Submissions * Abstract submission deadline: January 19, 2024 * Author notification: Mid-February 2024 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=3Dhottuf2024. Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Registration Registration is mandatory with a deadline of 8 March 2024 (AoE). Registration information will be provided shortly. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Program committee * Pierre Cagne (Applachian State University) * Evan Cavallo (University of Gothenburg) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Eric Finster (University of Birmingham) * Daniel Gratzer (Aarhus University) * Mitchell Riley (NYU Abu Dhabi) * Michael Shulman (University of San Diego) * Kristina Sojakova (INRIA Paris) * Jon Sterling (University of Cambridge) * Andrew Swan (University of Ljubljana) * Jonathan Weinberger (Johns Hopkins University) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Organizers * Evan Cavallo, evan.cavallo@gu.se (University of Gothenburg) * Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham) * Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi) * Jonathan Weinberger, jweinb20@jhu.edu (Johns Hopkins University) --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOOoPfWAgye44iHW_zR-a_oX%2B4yc6UKxFYSF1kdSqmmAK_xHSQ%40= mail.gmail.com. --0000000000003f6edd060cd3d2e1 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D2ND CALL FOR CONTRIBUTIONS AND PARTICIPATION
Workshop on Homotopy Type = Theory and Univalent Foundations
(HoTT/UF 2024, co-located with WG6 meet= ing of the EuroProofNet COST action)
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

-= -----------------------------------------------------------------------
=
Workshop on Homotopy Type Theory and Univalent Foundations
April 2 -= 3, 2024, Leuven, Belgium
ht= tps://hott-uf.github.io/2024/

Co-located with the WG6 meeting of= the EuroProofNet COST action
April 4 - 5, 2024
https://europroofnet.github.io/wg6-leuven= /

--------------------------------------------------------------= ----------

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 hom= otopy theory. Univalent Foundations are foundations of mathematics based on= the homotopical interpretation of type theory.

The goal of this wor= kshop is to bring together researchers interested in all aspects of Homotop= y Type Theory/Univalent Foundations: from the study of syntax and semantics= of type theory to practical formalization in proof assistants based on uni= valent type theory.

The workshop will be held in person with support= for remote participation. We encourage online participation for those who = do not wish to or cannot travel.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D
# Invited speakers

* Rafa=C3=ABl Bocquet (E=C3=B6= tv=C3=B6s Lor=C3=A1nd University, Hungary)
* Matthias Hutzler (Universit= y of Gothenburg, Sweden)
* TBA

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D
# Submissions

* Abstract submission deadline: Jan= uary 19, 2024
* Author notification: Mid-February 2024

Submission= s should consist of a title and a 1-2 pages abstract, in pdf format, via https://easy= chair.org/conferences/?conf=3Dhottuf2024.

Considering the broad = background of the expected audience, we encourage authors to include inform= ation of pedagogical value in their abstract, such as motivation and contex= t of their work.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D# Registration

Registration is mandatory with a deadline of 8 March= 2024 (AoE). Registration information will be provided shortly.

=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
# Program committee
* Pierre Cagne (Applachian State University)
* Evan Cavallo (University= of Gothenburg)
* Felix Cherubini (Chalmers University of Technology/Uni= versity of Gothenburg)
* Tom de Jong (University of Nottingham)
* Eri= c Finster (University of Birmingham)
* Daniel Gratzer (Aarhus University= )
* Mitchell Riley (NYU Abu Dhabi)
* Michael Shulman (University of S= an Diego)
* Kristina Sojakova (INRIA Paris)
* Jon Sterling (Universit= y of Cambridge)
* Andrew Swan (University of Ljubljana)
* Jonathan We= inberger (Johns Hopkins University)

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D
# Organizers

* Evan Cavallo, evan.cavallo@gu.se (University of Gothenburg)
*= Tom de Jong, tom.dejong@not= tingham.ac.uk (University of Nottingham)
* Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu = Dhabi)
* Jonathan Weinberger, jweinb= 20@jhu.edu (Johns Hopkins University)

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAOOoPfWAgye44iHW_zR-a_oX%2B4yc= 6UKxFYSF1kdSqmmAK_xHSQ%40mail.gmail.com.
--0000000000003f6edd060cd3d2e1--