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.8 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,URIBL_SBL_A autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-qt1-x840.google.com (mail-qt1-x840.google.com [IPv6:2607:f8b0:4864:20::840]) by inbox.vuxu.org (Postfix) with ESMTP id 8AE9431AE2 for ; Fri, 20 Dec 2024 01:37:31 +0100 (CET) Received: by mail-qt1-x840.google.com with SMTP id d75a77b69052e-46790f78a74sf192841cf.1 for ; Thu, 19 Dec 2024 16:37:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1734655050; cv=pass; d=google.com; s=arc-20240605; b=BZFAUesn7vCDr/ho7Dyj+KGQfAhdHJngbwsAm6JYo20+6rRy9XxF84PEXUjpb23m/z CgOddMT+nHAyqEvFDkzTYiLTeavi45X/ZLvqch8fwMw6F8KQYSGRUcEXgz3gP1UKZwDz paxd1b7NAb55+RHpU8rUCreJVyuul4TTcJ3L80pGroAfqrMz+rpUmi4C0lB78kWn52Aw agaboY8/hz8bu+Q6BLq+gQMorqfU4S5M4Te/jPMf6Whl/2UkUbqQ8IaoxHDbZ8Jx8BSW T4sui1ZvKwDh4VWDqRwnKEpE+x1UZQz8WLmrHfGXFFiYT5bMzmqgXA+hicSdcYfpq8Gt ylPQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=list-unsubscribe:list-subscribe: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=92i0RlnjrE2vqkgfHamTHVseZa2+w11ldMCz9EzFbDw=; fh=fJ0CkTSacslNlhyvmLmDtQ8btbRyWdsyzdWLl4DN/AA=; b=WOwea43tp+Dgvqq4EEHEcB37Q8msFkzB3r9vzr66MSbE32CAhCD1ZmXKotIgE8YNke 0aaQFO1+XjMInLLqzdDhWHpPyf4xN1nj9DRz2+E2CFGBBHCDOGaOJ6kEq/rI3t/CeXE4 0+wPbL51ctgSVWW/ciV4XztT0zvEjhyrw2Q/05yV6lkmlU9LlqXuirzwqloZn0l8v6HK eE9e9+vL7G2r/kp1W2zm5VYxKHUWb6ZIxGrBpSq0I0/AYCxnpGws1Wx0PHT9YJUb+K/Q hblEIFX4lfr40WasVNKOsiHGlEohhxvHMkseX/qCa+0irjEhXHRmX0H3no85wE3aKLZ2 NYsQ==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=BR4gf3wB; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=danny.gratzer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1734655050; x=1735259850; darn=inbox.vuxu.org; h=list-unsubscribe:list-subscribe: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=92i0RlnjrE2vqkgfHamTHVseZa2+w11ldMCz9EzFbDw=; b=CPQaP2EH6A24YfbbwMJtY7VOS2pUEEXWXUDsFLiLeRm+VBuHnU9aMwyKgG9pa5EFj4 uPGtoZ43mfNR2RfPeTRZ2EN7G+nycVvU7m/URsqWwiLWfHkfdv/v9vgUf5cZEgWG+fDL YSWp6NpCPO9riolaExpjcjSX7CT7Kk6F4z3ECuo41K6KMSjk3whPF2sgeuZxbeoIEOgD Fj7HESO1TFDQB2a8f7I+ALbrsEnU+7fZvOVguiegGDlC7HeoG9/RskS96SEP18F5ejKU cdv3fNhqd9upAV9VPSUMDCuKPbUIzCxkFjYcDxVhRKjoaihlcsxnRxB04xnOhaiNLh8G Velg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1734655050; x=1735259850; darn=inbox.vuxu.org; h=list-unsubscribe:list-subscribe: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=92i0RlnjrE2vqkgfHamTHVseZa2+w11ldMCz9EzFbDw=; b=kN/kyp78FNIDcnhCri2sMvEqpTFJHNIpqymgxUM+16E2jHQ4ICW7gn9e9fuAmoArz+ 0C6H5ALIZLQ8NVlSeSP6tN7M0J/nnRD5fhBtCoUk3QJSssu6WXpHjzLygSseQSRjPoRu S8wuVhqQDzQznrntLrPhpobdDiDB2oyIDA86PxXWr3VMXfLNgRw+dFEYbk2z2xxdLhlk lwGW92MKd7BHexNGYjyRRvDJ5dtHZ3gGaVVTVq80y5b03EauYrH1/VlZXqWtP59VloZs 9v+G3SMHnkBhfr/e9P07S43W5MsZJDW4LPcxKaCsx2DjpyaPCsooyrzdRs4H8j7wVcsz 8CCQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1734655050; x=1735259850; h=list-unsubscribe:list-subscribe: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=92i0RlnjrE2vqkgfHamTHVseZa2+w11ldMCz9EzFbDw=; b=QxCQOr2aNH9UfOPoU+4d03x+sIYXram9ACUwnojt96aPy6pRxUJ2R7IMppuCxXTee2 DkgRrx3SkXLCOW2zuVOBS2KbAR6YayB05YM9iZpwLRH6WZYhM8VJMDLoFyEpc9ZLUmYb RdbQCRHe9Vkq3BpyDM1R/YNQQB1RgxQ1UbLQm1nakvfoLN4EnDXH5C5GCqQif1ZnIPct ykIJiTOu1DdNInrP1kmBTF45g08qHhdKOxUO2FMFLi9VFlqnWKgXXycQTICFY1bt7qyt tr5aysSfLbK4P8eEUHTCDnSbYS04585OvXXanUmq6O5d07CPPJewW7LXlq9GnnX0UK0F mS9A== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCVvvU8SDTA5FoWhZuN051ISXQwuJsTGVqQazwrjuCXYmnrxGrF3thSJESyQqYNdsPN9iw==@inbox.vuxu.org X-Gm-Message-State: AOJu0YwuZh6XddjagqVC3PtHnle2P4RXGzR1uR18S1RnRmXf7NZBKiNq RrUnGkmykWYWGhAOEgWD5HixxBBHzPxC/beLMnG6m+m5Phhx1hQd X-Google-Smtp-Source: AGHT+IH7ulrfKOL/AXKbeBDufKfIy86I+TkDYLle+oOW4xV2rg/YzeEc0HEQuNZcesLGfoTTlu00WQ== X-Received: by 2002:a05:622a:130a:b0:466:975f:b219 with SMTP id d75a77b69052e-46a4a8d36b5mr1227931cf.8.1734655050130; Thu, 19 Dec 2024 16:37:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:1189:0:b0:467:77d8:69e7 with SMTP id d75a77b69052e-46a3b18266fls22466771cf.2.-pod-prod-05-us; Thu, 19 Dec 2024 16:37:27 -0800 (PST) X-Received: by 2002:a05:622a:1aa8:b0:466:a308:292c with SMTP id d75a77b69052e-46a4a8e7181mr19726821cf.32.1734655047091; Thu, 19 Dec 2024 16:37:27 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1734655047; cv=none; d=google.com; s=arc-20240605; b=g8A05KsRQWrz81xKiFoZp6HbV4Cev5r+XObmBQe7DPm4hOcO9nr/hy7j688WkHvfCI pMjeOvmBZxcYD7+DWxpkSB2m/ED3CYCKlZhgkvmj+upqLEw38kzg4DurtfsM7DUuHUt3 t62v6PigpDNWezeF2Z82fseRQmyGMMqo0BIFFeY1bsJi8DVCH9oqridf0mvRgKSH9gcn CKlP8eyN1fgzRRYvO4xQ2CQ9jAw3j6wCC4TFzidRA8iEHGjXbqNjBbIc9+7sAEgRcokq iF7QRnc2SsfGGxe8tPdJic8yD0EsR2S7xSOmiR29OBpqNJsqUwDhR/3ZFBhDcAAoLE7P YutA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=GzdcPR2xV66smGcQ9PX8elRbPkrndtjm69kddTHcfHI=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=blg3NMcp1V1HZLZvZXboYlRVCJb+SgM+unvqyL1No8yR3smvdALHAz7cJRFiiDh5rs gY30wXDG400Brwbx+IaJelCHhLYuOJW1//hPYgELOUEQRSut0dL+Oq6+h783eOmRUZew qSC1DiPSdVw6XLUfUKyJdLRtSU0eMhqhzl9LStyXO4DiEZHPF2jhXR6bDTJPBtW6g2Jd 1H9SDyc2w+IFlhdnSspYRLyuqULmGbraEUCoc/5GDrl6ouCiTteZoaaWnfJBdRgPs/FB jgIV2NyCZTYIitsAGV5aIZIl0ZgPyU56YJE7NBRgxZB/G6e/Pq7DnrUJydC8bBrqUMx5 W/cA==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=BR4gf3wB; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=danny.gratzer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id d75a77b69052e-46a3e4f9c59si1143321cf.0.2024.12.19.16.37.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 19 Dec 2024 16:37:27 -0800 (PST) Received-SPF: pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id 3f1490d57ef6-e3988fdb580so1179418276.2 for ; Thu, 19 Dec 2024 16:37:27 -0800 (PST) X-Gm-Gg: ASbGnctf3vpuXoFBsKDTr4R2O7VfrfvlMaxFIFPohJ6VqNFnyO2ws+jw15HNTK2+4/h lXqds/4FQm5KOIzZL/t07vefGrmL0TjCka3ZP X-Received: by 2002:a25:ae52:0:b0:e4c:1b6e:593a with SMTP id 3f1490d57ef6-e538c3d6ed2mr838476276.33.1734655046379; Thu, 19 Dec 2024 16:37:26 -0800 (PST) MIME-Version: 1.0 From: Daniel Gratzer Date: Fri, 20 Dec 2024 01:36:50 +0100 Message-ID: Subject: [HoTT] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000d8f57d0629a8d942" X-Original-Sender: danny.gratzer@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=BR4gf3wB; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=danny.gratzer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.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: , List-Unsubscribe: , --000000000000d8f57d0629a8d942 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Apologies for any duplicated messages. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=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 2025, 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 15=E2=80=9316 April 2025, Genoa, Italy https://hott-uf.github.io/2025/ Co-located with the WG6 meeting of the EuroProofNet COST action 17=E2=80=9318 April 2025 https://europroofnet.github.io/ ------------------------------------------------------------------------ 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 * Reid Barton (Carnegie Mellon University, USA) * Bastiaan Cnossen (University of Regensburg, Germany) * Ambrus Kaposi (E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Hungary) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Submissions * Abstract submission deadline: 7 February 2025 * Author notification: 10 March 2025 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=3Dhottuf2025. 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 # Program committee * Ulrik Buchholtz (University of Nottingham) * Pierre Cagne (Applachian State University) * Dan Christensen (The University of Western Ontario) * Felix Cherubini (Chalmers University of Technology/University of Gothenburg) * Tom de Jong (University of Nottingham) * Jonas Frey (Universit=C3=A9 Sorbonne Paris Nord) * Daniel Gratzer (Aarhus University) * Philipp Haselwarter (Aarhus University) * Andr=C3=A1s Kov=C3=A1cs (University of Gothenburg) * Anja Petkovi=C4=87 Komel (TU Wien) * Lo=C3=AFc Pujet (University of Stockholm) * Mitchell Riley (NYU Abu Dhabi) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Organizers * Felix Cherubini, felix.cherubini@posteo.de (Chalmers University of Technology/University of Gothenburg) * Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham) * Daniel Gratzer, gratzer@cs.au.dk (Aarhus University) * Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi) --=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 visit https://groups.google.com/d/msgid/HomotopyTyp= eTheory/CACbeAXCg8i8wvd9jESEEtSGB1ArORf8Bd5cfk6svqLiLGnCWzA%40mail.gmail.co= m. --000000000000d8f57d0629a8d942 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Apologies for any duplicated messages.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=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 an= d Univalent Foundations
(HoTT/UF 2025, co-located with WG6 meeting of th= e 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

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

Works= hop on Homotopy Type Theory and Univalent Foundations
15=E2=80=9316 Apri= l 2025, Genoa, Italy
https://hott-uf.github.io/2025/

Co-located with the = WG6 meeting of the EuroProofNet COST action
17=E2=80=9318 April 2025
= https://europ= roofnet.github.io/

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

Homotopy Type Theory is a young area of = logic, combining ideas from several established fields: the use of dependen= t type theory as a foundation for mathematics, inspired by ideas and tools = from abstract homotopy theory. Univalent Foundations are foundations of mat= hematics based on the homotopical interpretation of type theory.

The= goal of this workshop is to bring together researchers interested in all a= spects of Homotopy Type Theory/Univalent Foundations: from the study of syn= tax and semantics of type theory to practical formalization in proof assist= ants based on univalent type theory.

The workshop will be held in pe= rson with support for remote participation. We encourage online participati= on 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

* Reid Barton (= Carnegie Mellon University, USA)
* Bastiaan Cnossen (University of Regen= sburg, Germany)
* Ambrus Kaposi (E=C3=B6tv=C3=B6s Lor=C3=A1nd University= , Hungary)

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
# Sub= missions

* Abstract submission deadline: 7 February 2025
* Author= notification: 10 March 2025

Submissions should consist of a title a= nd a 1-2 pages abstract, in pdf format, via https://easychair.org/c= onferences/?conf=3Dhottuf2025.

Considering the broad background = of the expected audience, we encourage authors to include information of pe= dagogical 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
# Program = committee

* Ulrik Buchholtz (University of Nottingham)
* Pierre C= agne (Applachian State University)
* Dan Christensen (The University of = Western Ontario)
* Felix Cherubini (Chalmers University of Technology/Un= iversity of Gothenburg)
* Tom de Jong (University of Nottingham)
* Jo= nas Frey (Universit=C3=A9 Sorbonne Paris Nord)
* Daniel Gratzer (Aarhus = University)
* Philipp Haselwarter (Aarhus University)
* Andr=C3=A1s K= ov=C3=A1cs (University of Gothenburg)
* Anja Petkovi=C4=87 Komel (TU Wie= n)
* Lo=C3=AFc Pujet (University of Stockholm)
* Mitchell Riley (NYU = Abu Dhabi)

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
# Org= anizers

* Felix Cherubini, felix.cherubini@posteo.de (Chalmers University of= Technology/University of Gothenburg)
* Tom de Jong, tom.dejong@nottingham.ac.uk (University of Nottingham)
* Daniel Gratzer, gratzer@cs.au.dk (Aarhus University)
*= Mitchell Riley, mitchell.v.riley@nyu.edu (NYU Abu Dhabi)

--
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 visit https://groups.google.= com/d/msgid/HomotopyTypeTheory/CACbeAXCg8i8wvd9jESEEtSGB1ArORf8Bd5cfk6svqLi= LGnCWzA%40mail.gmail.com.
--000000000000d8f57d0629a8d942--