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=-0.6 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,URIBL_SBL_A autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-oo1-xc38.google.com (mail-oo1-xc38.google.com [IPv6:2607:f8b0:4864:20::c38]) by inbox.vuxu.org (Postfix) with ESMTP id 9129D2B412 for ; Tue, 16 Jan 2024 15:11:28 +0100 (CET) Received: by mail-oo1-xc38.google.com with SMTP id 006d021491bc7-5991858e3e7sf701462eaf.0 for ; Tue, 16 Jan 2024 06:11:27 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1705414286; cv=pass; d=google.com; s=arc-20160816; b=quaSUb6OuHDzuYvVEdFXJBllykBP+laR3DCGpuD3RzPRtttVGzWbNHI2A79NBLkQf6 alGuak40+dP1MIUjpAC64PFL7l/4ZtmF1TZ3gHFbXBtOzm7pqzDRh7/tmS8OzBT41KUU Yo9T/k0EvpAErMhOWjVPLu64679Pdy906SP6FitwZ1uGeYMrFa87RC4pKq27VusV5W6y yPQmrka28j9UyCit8uwFz46TQ+y361BkhXfSW182/4KJyBcOuQlM+XHVeuBG3twiG4W0 5fcIbXG8uOXELf2kfsoPi5+me4Mual7dopUUu2UGLjmKpPnTK7Z93urLqrpNfVo1eOTj /iUA== 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=PdVrne7YAMs5r1mCEs7CukPdDo7CfyIzFqsD3Whm8vo=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=Jev8NUF9LgoICZisvsxBmpQx2FtqElpZhj574cDClv5TLbqsuX2EgIF9E7opH85fb9 1sDFJxhOcBrHK9TnHfM+dSqmhCrtw30dmi3+1R0uw+C0UZPmLzFzALafGKJdGIx+xT/t QUgdOcHY9dngP5JmgEHj5NL/IyMdV/cvTgY3OJPPGgFBxWCNmKR/naKSHd6H9deGw5e7 xAypT8Guih8dg/1GljSVHJEQ/ssItEuEVvEGRGYSe2Cc3Im+K2nVWw/GWeyDvmHk9Zda An7sDsy1eEGxzSKV3usdP9c66u7n8ec5SBKT3cAG4suJx9gUyGlU1s1v59A4Ne7vxpku z3Qw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=FU+lp4Rx; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::62a 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=1705414286; x=1706019086; 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=PdVrne7YAMs5r1mCEs7CukPdDo7CfyIzFqsD3Whm8vo=; b=xrIRSRZQnHefEm6AdyXJtH4rbMRUAbEsChAz2/kR6ID6MXYFb3CvMJv0oNLOWau1KS QG3yEK0HcHW60JiWJc4SPcASVeZq/crOPCmfl5bUAoV8Ll9gPjXg+KZWa+maqrdHXp4A Y6rmlVHPgacpppMWWBF0kbvq0/5I3K/oyGdqJuun7B2PLlVzjYyTDGC0Vm8ELjLZQIH2 hbT1r0PjF+KECe4ClX9YjWqozSuOD6Vkgl6G/xDrO5AgURABcUIdE2zHMYAyD7BQCs6k GKTmkBCzpYiZZltXCYfxYJDJusPdM+p6HH4aYkLxxfY0QXu1hIMsHWL+rTlQUY3X/FvM NzaQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1705414286; x=1706019086; 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=PdVrne7YAMs5r1mCEs7CukPdDo7CfyIzFqsD3Whm8vo=; b=cjGXY2oFp3Ouv6S61NEl2Fg+hsv4+C53hz+NxGvUomzyi5TEPnL4gYByCR0gZVK5+t 0Zh5nssmUl8qEQyayM6TL0kq/NY2t6E/3crMv5LQiwXgl61S3SRN14oxywnZhZytd9IB pgl2X6OMQ+CV1QiaEmHYFyrAWpzTd9Qm9bN9UuB1Vbu6TYvHPevI6nfqS4rUa9Z0UToR Do+ihc3+FZxn3Lx0UYonv1bABOQajHORvhw5GdIiciUZ5j3H2z47zNl4wrr5TyAvvSKU YXzNGg1EiL96FzqHCYFizNzlo+9hmggVVDkMp6Etk22GpPR8MieAVDCrhkcyaj4msjS7 Y+DA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1705414286; x=1706019086; 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=PdVrne7YAMs5r1mCEs7CukPdDo7CfyIzFqsD3Whm8vo=; b=bH5FVulxTmakLlTAIsjWPBXAqpG3tDHVbY3TUyernQ1an+mcMDGzhvnPyJgdFIaOJU uVAcyhmIzzIjuE+P5aiDoBVVqpu7w8cwsb0U3q6k61QqGuIlJsIOcOqW5zAKWXT8tVSu TR/pHQyYkKdhTcpT+GvJuIvx5QmvB9+4gvshWK/WhG2kIlgck1nOgZ8OGl7V7cI4xuJO +C2BJSYUIcjhdkkK608L1OOb6r4gIcMeggDIAXY1JV12i+piVrkcmVvSJ1aCbBxQb33b D026BZXuw6ggE4QkHqJDuBZuCBKiU28jFwSSVuSWT+Zrs0Nhd4wRVF4/w2iuQTHU0tqp E1fA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOJu0Ywh8qIOtroBf6mT2nikNvHOjviVW8y0uZvQIq/NlOqFK6C4vM2o N0yT0R8bxhUtVOsaWtHFIEI= X-Google-Smtp-Source: AGHT+IFFevCHtZoogFaoPJrL4FgkPrbITIzldjClTUeowwb52JRzXSszf1xhheclfx0ukUmMskLCxA== X-Received: by 2002:a05:6820:609:b0:598:75ef:175b with SMTP id e9-20020a056820060900b0059875ef175bmr3941290oow.8.1705414286362; Tue, 16 Jan 2024 06:11:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a4a:5a85:0:b0:598:dc0d:33b6 with SMTP id v127-20020a4a5a85000000b00598dc0d33b6ls2613189ooa.2.-pod-prod-03-us; Tue, 16 Jan 2024 06:11:23 -0800 (PST) X-Received: by 2002:a4a:aa0b:0:b0:598:bd0a:a1d8 with SMTP id x11-20020a4aaa0b000000b00598bd0aa1d8mr3329337oom.1.1705414283304; Tue, 16 Jan 2024 06:11:23 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1705414283; cv=none; d=google.com; s=arc-20160816; b=G8oh1u0Uo5f7quAAWInk92/j87r/0V3SDStGeRt3sBoSTlRWF+EPif8oWgQfunUr+d GZoRBcytqphjNpPF3RNq8Nw7BNowvD8PFDr6z/UfZOfFSbndb4PF7ndvCjLU+ljxh+NI Pj28L4B6QySjMREkhO6NaIkoqr29iP338COQ+AvN9GDIGP7SSx/KrzTUKmG3u/QW6ieX XcE+YlelKlygYVt4qUP+jIsYjFStnHoa2qQ21p4g9PPuxiEwtLqlxqFRydYR/r70g1LJ +kxf9h3XsPqXXQXcokwsjED/lrOFeNebY9iyF9ru9tPqurduoWVpyznjVmaFuTqMCAkO +h0w== 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=T3IKnTPhovSnl9f7Pci5X6dMICWGrr7N3n59tVYJc5k=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=Hk6RhDIztKqcNCkQ+8P46uRLg8oJ/7X2UVuS9p4RoXHvEiuYGGot80mQb7Fw+c2ykG 7Zl3CqNPkY+rDZknktbwGf/vGPnlpBbnMGPpxfdV/IgDS4K/EAy/GQtsfWiYzWMu9xw6 0KvCI45V9GNACKnqH06IUSQ2qH72UPdlhomOLhe+AGR/zhgd5ZQWf1j8NDYHVAxmuOFd t1TCnSEYolhTMT/chzkEY93Xuh5K2d0LxsnaWV8bzKBEOnPCzVvObX1x0Zw0EI4LHAsa gq2ViyAHCuA6nhNezSxfPEZasXfxjz0lyaodmECdWegpqjwywS4MZOEdLACYNs/OB0hk hJDA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=FU+lp4Rx; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) smtp.mailfrom=weinbergerjonathan@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pl1-x62a.google.com (mail-pl1-x62a.google.com. [2607:f8b0:4864:20::62a]) by gmr-mx.google.com with ESMTPS id g3-20020a4ab4c3000000b00598965e5d7esi811792ooo.2.2024.01.16.06.11.23 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 16 Jan 2024 06:11:23 -0800 (PST) Received-SPF: pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) client-ip=2607:f8b0:4864:20::62a; Received: by mail-pl1-x62a.google.com with SMTP id d9443c01a7336-1d480c6342dso75073475ad.2 for ; Tue, 16 Jan 2024 06:11:23 -0800 (PST) X-Received: by 2002:a17:90a:39c8:b0:28e:719e:6688 with SMTP id k8-20020a17090a39c800b0028e719e6688mr825504pjf.83.1705414282717; Tue, 16 Jan 2024 06:11:22 -0800 (PST) MIME-Version: 1.0 From: Jonathan Weinberger Date: Tue, 16 Jan 2024 14:11:11 +0000 Message-ID: Subject: [HoTT] HoTT/UF 2024: Final Call for Contributions and Participation To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000842cda060f10b497" 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=FU+lp4Rx; spf=pass (google.com: domain of weinbergerjonathan@gmail.com designates 2607:f8b0:4864:20::62a 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: , --000000000000842cda060f10b497 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 FINAL 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/CAOOoPfVsMQAZRLt2N08j8WoGLhWz7H%2Bw%3Dkbj3jYZ8D5z%2BfJuc= A%40mail.gmail.com. --000000000000842cda060f10b497 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=3DFINAL CALL FOR CONTRIBUTIONS AND PARTICIPATION
Workshop on Homotopy Typ= e Theory and Univalent Foundations
(HoTT/UF 2024, co-located with WG6 me= eting 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= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAOOoPfVsMQAZRLt2N08j8WoGLh= Wz7H%2Bw%3Dkbj3jYZ8D5z%2BfJucA%40mail.gmail.com.
--000000000000842cda060f10b497--