From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-yb1-xb3c.google.com (mail-yb1-xb3c.google.com [IPv6:2607:f8b0:4864:20::b3c]) by inbox.vuxu.org (Postfix) with ESMTP id AE3B3212F8 for ; Wed, 21 Feb 2024 15:45:36 +0100 (CET) Received: by mail-yb1-xb3c.google.com with SMTP id 3f1490d57ef6-dcc58cddb50sf1208803276.0 for ; Wed, 21 Feb 2024 06:45:36 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1708526735; cv=pass; d=google.com; s=arc-20160816; b=R2yxPRrCFi5QiE0Ff5zjOV6NYvGJmbZiLMDaVfWKy2xzhes5035wanj34bNd1I8set 7nNUj+7pQ3nqklXdjiaQAcjyC6lLeAEjE5me3zg5MM6QwqWV+vzVIDZgxTnwO2A/xc6C ZW5r/DZpSXWN1lnRmNt/IoUVpnU4r4Cm8pxar7WSxOjlAIGsMyM0z+QJ5fB3aaBs8aYb iU2ZXEXUdZ+nZXC6uC7wiDIzuvWA6GZQgF2WryFoOzg5iPwOwa2AAywsDYZoLlYyvpi7 PUTFVte62uKhPUaP9HiUZ+xLUYp7eTPR9O9alAcpiw/p8LlmGNkQtoX7L4pwr7LDyDAO pEJA== 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=iLoO+fmB1G91eqJOp8J9SscUKeke8XARIA5SA/k331U=; fh=W19ycEIbq+XA1lFzQ5kMN4fZRnZCeXuejoumnRNePUY=; b=o5QVJOAVxfn/3B8EKPeMlMTL9czg19rsN3c+uiXazyjQO39JEnFuQAtMlAVk3ue2Xd AiyEps1cn1hYOrFr6hh0dblq/bv0vkJNnneI/KwHd6pcfe1qDKtayorc322WlDpN+mYx qjuArGw+k06xJWs9s8mfVoshwdwc31UBUuOW7PC5GxEfxHasYJAkQl45woUmceLXzVlN FQ+ARFOzNbc42d2mLcQoFT7yfcCO3t91Uh4wAfCkHC/WqdVcERAWE9k2cK6CkZVawRRX Wcc9swMBNfmmrPojDP2Oj/RIzU/xp11qtLy5snm3Cg10RlRBgBPp08CFbr6wgGXAlCiO +H0Q==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=mV8BAo0N; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::102a 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=1708526735; x=1709131535; 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=iLoO+fmB1G91eqJOp8J9SscUKeke8XARIA5SA/k331U=; b=PvFZW24soGt90MLma740yK+tga9It+0/omLyl1FqGkBI7DN8WnXqXysk4WxOLMVd3a tgMY6Me9R2S7SqF3WdWYeWtngYIa66wHQ5WFTqRzUqL5B5aTh583wXv783llZZ79qScY 9iDfhS8A4QhoOIBKp3m8b6xhCd3bcRn7Sk3PfFD6vMTknghCAHDRT3A7B04drk+sjySI dheUyuTuTn9fP+kR10yhdg5anPaTwI8nmos6vAOvuQZd1t2mz8Z/w9eBrgrLIczDhA0C kg0fve7vAwFUE5rZewXt5k+3kMSoTzLqB8AtmxjK/rHEoUdzcO4OOQQMYlFitwXH5ys0 MIBA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1708526735; x=1709131535; 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=iLoO+fmB1G91eqJOp8J9SscUKeke8XARIA5SA/k331U=; b=N/eXS4xQcwCrrKJv81hdUhmCR2bfCCAX2xAnCiMOlUQmHEfRQkIa66RmagySC8tKTN +Q46iBQXmdG7h/DL0yxDcg3+pL5GU/PDbmuX+3XqfZuadh1Qz0rgNT16dKwgQ3QDaqOP b/JnAjT5B32Pe1q0dxiLg21HKKF06Y3m8oh8RYkCQnVaafGbJgPac72zhWTocbjQBrdg Qnr0zPPO5uYYP9i+qWHqjIXWbBZDSuhTLu9dpgxIksjarGcieuraQAeOwD3puxGi+gCM ywgm6GjTs24jp0WhHMfjBCobnrZOprr31SiWcoll8u8dDGql6kiZkII+Clx+1mVMx2u+ rGmQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1708526735; x=1709131535; 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=iLoO+fmB1G91eqJOp8J9SscUKeke8XARIA5SA/k331U=; b=mFbEnu0dHoEIE1HQYfBNIPPE7c60nX41U9/u9Gxa+ND57dCm3MTpwpLwVHXme72rd7 vq/E6yvAb7c7dwvcMT64c2Ja0Ph7ivx7FxgDPTuskypmtA+LTOT+RX9hzU1EgOQZ9dze N6N6misKqqzfF4H4tcHOEMhQknDzcJBU4l2nxIjhtXbYmz3FR2A9fXsk61HhHHhi059T IugwSCur91LGAU8TCQE1UHIGgWot9CcQ/kpRw+EnBCDJfZxFkKrl+ZaKgEN5t0oaQZTG QcOkHdLHydJRNsD7SY2y+sYmFBCEpO9lA6cOn6EY/+60BlZJ32UUDR3TTyNjXfkIs3Nu wF/A== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCWyHFIQZQQnbyKNjrbwElg+Aqk2M1Vg+KOwaq0obp/ZvPtSBaHIFHts9O1Hb3z0MdyNsTJ/SRlLG8ksXVjda92bmA== X-Gm-Message-State: AOJu0YxKOzJCYINeiyc1JcV73ImMId85OG5GNeJCduc9frs8RlKRT07Q YwVi2reHb2nSKMTTkoNOGk7Jv18UdgESu+ETEH3zKE8uDqI0jWh0 X-Google-Smtp-Source: AGHT+IEqoLtRqMyjGLoqMZfsUPKBsXlszEdFaQRl7GLMdiPNo0DTXg8O3RkrFTR/VdD8SbNLerMdEQ== X-Received: by 2002:a05:6902:4d3:b0:dcd:5635:5c11 with SMTP id v19-20020a05690204d300b00dcd56355c11mr16895364ybs.45.1708526734516; Wed, 21 Feb 2024 06:45:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:d88b:0:b0:dc7:4363:dc02 with SMTP id p133-20020a25d88b000000b00dc74363dc02ls2149223ybg.1.-pod-prod-06-us; Wed, 21 Feb 2024 06:45:32 -0800 (PST) X-Received: by 2002:a81:6c14:0:b0:608:68bc:6b8b with SMTP id h20-20020a816c14000000b0060868bc6b8bmr4310564ywc.52.1708526732499; Wed, 21 Feb 2024 06:45:32 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1708526732; cv=none; d=google.com; s=arc-20160816; b=C1GJKGFJo4hed6+5EBSVPoRC/0AmKe3vF9koOQnnZxf2xtGi0xhde8liyPDP8X/Qn+ DxxZxx7/V7iwubx3rzuxMHT+bKm2KQ44vJmNl1MOwJdtQkRYR8KHr1s1xvTNlvjS8X9G yz4j8A2oeohs5ySra/JudWxxhEPayIWb/LlMyF3EkW5arbeSkUdSUl9fKAoOwmF+3PR5 x/S9qOGCn/BqcXLMj/t+5tkJw+zazwkSAUux/7fMnSR/LCZBK1ipYWa6bo10mehlHyOh cP4yzj1LWenEQ0XbJoRZz0ZzOUlVROhsw6O0hFRuAPMvz9/1A06SyRJJ8sUWqb0STzZP uleg== 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=YSxUm7c2tTkxoTQDLspCah5hl6TJ09hR44A0BluOgAU=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=LpfDNylzdMaBudzFK4fLIHVDcLFBAuJql7S8aTu+iyn+HUcWfFte/AB/QPyZZGuLOs PP3t+Ty/KKzYODFUbQrRdO+mkQEYK/y9C61Cuy6Et0/oNm57PraOX3+3W97vkFgajfw8 0RILdmgAPgEYSLAYHt5vT8K8MoJlq1ZWT0efycQUd8/fV46g2h5M96aLkE1Y62cCzGJw wNabSLTJLDN2boYGV+Zf1qIXe9occsHv0HKBzFKgYOqjJYef2DYAR++2uWUaU+WcQzKt qbuE3ZUYzkxqg/xdevjQWid7qkw7uMQmDe9RrEd3p+YvW8mHCXDKMobChEUR4J7ZOvju buPg==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=mV8BAo0N; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::102a as permitted sender) smtp.mailfrom=weinbergerjonathan@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pj1-x102a.google.com (mail-pj1-x102a.google.com. [2607:f8b0:4864:20::102a]) by gmr-mx.google.com with ESMTPS id w64-20020a0dd443000000b006088733eff3si109708ywd.0.2024.02.21.06.45.32 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 21 Feb 2024 06:45:32 -0800 (PST) Received-SPF: pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::102a as permitted sender) client-ip=2607:f8b0:4864:20::102a; Received: by mail-pj1-x102a.google.com with SMTP id 98e67ed59e1d1-2999329dfe7so499178a91.0 for ; Wed, 21 Feb 2024 06:45:32 -0800 (PST) X-Received: by 2002:a17:90b:3609:b0:29a:1c50:6d43 with SMTP id ml9-20020a17090b360900b0029a1c506d43mr1416801pjb.27.1708526731501; Wed, 21 Feb 2024 06:45:31 -0800 (PST) MIME-Version: 1.0 From: Jonathan Weinberger Date: Wed, 21 Feb 2024 15:45:20 +0100 Message-ID: Subject: [HoTT] Call for Participation and Registration: HoTT/UF 2024 To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000eba62b0611e56031" 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=mV8BAo0N; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::102a 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: , --000000000000eba62b0611e56031 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 REGISTRATION FOR 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 # Registration Please register by filling out this form: https://docs.google.com/forms/d/17WFBrTRoa9f3ZkKDpDlPAQFwvEFTreOAqbxC4XWLO1= 4/ Registration is mandatory (also if you're attending online only). Registration deadline: March 8, 2024 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Invited speakers * Mathieu Anel (Carnegie Mellon University, USA) * Rafa=C3=ABl Bocquet (E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Hungary) * Matthias Hutzler (University of Gothenburg, Sweden) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Contributed talks Authors and titles of contributed talks are listed on the website. =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/CAOOoPfUTFp8JWjj6qbA5isUA%3DKFKgUFeYHVSPi%2BUy9zEssc6CQ%= 40mail.gmail.com. --000000000000eba62b0611e56031 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=3DREGISTRATION FOR
Workshop on Homotopy Type Theory and Univalent Foundat= ions
(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
<= a href=3D"https://hott-uf.github.io/2024/">https://hott-uf.github.io/2024/<= /a>

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

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

Homotopy Typ= e 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 Founda= tions are foundations of mathematics based on the homotopical interpretatio= n of type theory.

The goal of this workshop is to bring together res= earchers interested in all aspects of Homotopy Type Theory/Univalent Founda= tions: from the study of syntax and semantics of type theory to practical f= ormalization 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 trave= l.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
# Registratio= n

Please register by filling out this form:
https:= //docs.google.com/forms/d/17WFBrTRoa9f3ZkKDpDlPAQFwvEFTreOAqbxC4XWLO14/=

Registration is mandatory (also if you're attending online only= ).

Registration deadline: March 8, 2024

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

* Mathieu Anel (Ca= rnegie Mellon University, USA)
* Rafa=C3=ABl Bocquet (E=C3=B6tv=C3=B6s L= or=C3=A1nd University, Hungary)
* Matthias Hutzler (University of Gothen= burg, Sweden)

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
# = Contributed talks

Authors and titles of contributed talks are listed= on the website.

=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 U= niversity of Technology/University of Gothenburg)
* Tom de Jong (Univers= ity of Nottingham)
* Eric Finster (University of Birmingham)
* Daniel= Gratzer (Aarhus University)
* Mitchell Riley (NYU Abu Dhabi)
* Micha= el 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 (Uni= versity of Gothenburg)
* Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham)
= * Mitchell Riley, mitchell.v.ri= ley@nyu.edu (NYU Abu Dhabi)
* Jonathan Weinberger, jweinb20@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:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAOOoPfUTFp8JWjj6qbA5isUA%3DK= FKgUFeYHVSPi%2BUy9zEssc6CQ%40mail.gmail.com.
--000000000000eba62b0611e56031--