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.5 required=5.0 tests=DKIM_INVALID,DKIM_SIGNED, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,HTTPS_HTTP_MISMATCH, RCVD_IN_DNSWL_NONE,RCVD_IN_MSPIKE_H2 autolearn=no autolearn_force=no version=3.4.4 Received: from MEUPR01CU001.outbound.protection.outlook.com (mail-australiasoutheastazlp17010005.outbound.protection.outlook.com [40.93.137.5]) by inbox.vuxu.org (Postfix) with ESMTP id 45301245DB for ; Thu, 14 Nov 2024 19:55:01 +0100 (CET) Received: from SmtpServer.Submit by SYZPR01MB7687 with Microsoft SMTP Server id 15.20.8158.19; Thu, 14 Nov 2024 18:54:59 +0000 Received: from SY7PR01MB8286.ausprd01.prod.outlook.com (2603:10c6:10:1ea::10) by SYZPR01MB7687.ausprd01.prod.outlook.com (2603:10c6:10:16e::23) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.19; Thu, 14 Nov 2024 18:54:49 +0000 Received: from MEAPR01MB4358.ausprd01.prod.outlook.com (2603:10c6:220:16::20) by SY7PR01MB8286.ausprd01.prod.outlook.com (2603:10c6:10:1ea::10) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.18; Thu, 14 Nov 2024 18:54:43 +0000 Received: from MEAPR01MB4358.ausprd01.prod.outlook.com ([fe80::ef9f:d02:9876:fa7d]) by MEAPR01MB4358.ausprd01.prod.outlook.com ([fe80::ef9f:d02:9876:fa7d%4]) with mapi id 15.20.8093.024; Thu, 14 Nov 2024 18:54:43 +0000 ARC-Seal: i=2; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=pass; b=bjfv/pUlQokypJHrjTVJTGIV5Tsv7xHaiB/zLZCWaXNK6yWefMHsQEPIC3uZDnG8N03OCK2pG1Njeh306XbLEAlnw9s+HQjjeZZkEjUVP2v5QeikrQQF9bL6fqhFDrU/S0vVHIHTRSnAC0CIX42KzICCwBYXvzuyF/nPEPpzC9Gl/lMRlHuFbBzo0Mg7QV/K/bJ3gsvJYaWpkWSBCu6xVwptUt4L0zmZYWab2cQ2dujtRcwffmfM90lF9sKjU12STgNjYhFH2kH9QVeVCLUOm7CmAUS8fG/3Pxecu6gy6iiKK88f9U1A1ZTW24oorh3nfOEZC3o9QonxNJGJJ2/wgw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=rnrBGTAM6xD6X/WNqkkuuzQyxFN+MBgV8J6lPq9HqIs=; b=GhQJZP1KpLTRKeI7EKTrwYAic8FGG2Zq5KIapXU/051wNTu7H/p2ZVMoMetQ1b2hoYUvsmUtUUnKAsa3tThD8AUleXu1ZLDEWRjU+W9XXq3KSJOdTAiSLM4ZvuQQ0nhLHV14kwdr+JGp5Rm/t7gSv05zcI45JUBr8DpCbUdK4/FysBj8uxvAL9zURWIDW0DNmLATEwUAiPl7LHzvVUQ/8pHBWyDoj2RT1uYT/bmGUpygFssSjGSVF388HvohlWNxO1D8Wj6m+3BBOf1eofc5MwVOAAQos+u0UcM/loKIceqEajqzsCJ8Ys3LZ4tScvlWv0f2Qr+Pp/kvYzk+oWcYaA== ARC-Authentication-Results: i=2; mx.microsoft.com 1; spf=pass (sender ip is 185.67.36.66) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=posteo.de; dmarc=pass (p=none sp=none pct=100) action=none header.from=posteo.de; dkim=fail (signature did not verify) header.d=posteo.de; arc=pass (0 oda=0 ltdi=0 93) Received: from SYYP282CA0008.AUSP282.PROD.OUTLOOK.COM (2603:10c6:10:b4::18) by ME3PR01MB6120.ausprd01.prod.outlook.com (2603:10c6:220:da::7) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.18; Thu, 14 Nov 2024 17:10:19 +0000 Received: from SY1PEPF000066C3.ausprd01.prod.outlook.com (2603:10c6:10:b4:cafe::b1) by SYYP282CA0008.outlook.office365.com (2603:10c6:10:b4::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.18 via Frontend Transport; Thu, 14 Nov 2024 17:10:18 +0000 Authentication-Results: spf=pass (sender IP is 185.67.36.66) smtp.mailfrom=posteo.de; dkim=fail (signature did not verify) header.d=posteo.de;dmarc=pass action=none header.from=posteo.de; Received-SPF: Pass (protection.outlook.com: domain of posteo.de designates 185.67.36.66 as permitted sender) receiver=protection.outlook.com; client-ip=185.67.36.66; helo=mout02.posteo.de; pr=C Received: from au-smtp-inbound-delivery-1.mimecast.com (103.96.22.101) by SY1PEPF000066C3.mail.protection.outlook.com (10.167.241.53) with Microsoft SMTP Server (version=TLS1_3, cipher=TLS_AES_256_GCM_SHA384) id 15.20.8158.14 via Frontend Transport; Thu, 14 Nov 2024 17:10:17 +0000 ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=dkim.mimecast.com; s=201903; t=1731604217; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: dkim-signature; bh=rnrBGTAM6xD6X/WNqkkuuzQyxFN+MBgV8J6lPq9HqIs=; b=pRG+2mEcd/QXwxnJiXvxlhWZ7/6oMscW4X/HDMFMxclwBl/izZPKHF7q8fqZCO+TSoSl+d K+ZFXsMj6w53eYC7TMeYWsU7qNbnMA7CYfKU3BbhfXGhjPV2Nf23wYwKnkpMCMBQvIC7Lt ouryXcuB62KCqvXPZr4Dg+1BEYOjV3Ev+MoXuJX/8bqb0a0CopzlhaCxkmhpv2RZYI4y6X tq2P4GzWvkR5aXvUCW0MPb3J706Eo+e14Tx6trQT5nhDqCHNL1eZeIRWYC0jPNBtPmR5Yt LozpQhtbvVs9zStbDkzO6OyDEhKh29VtBg4+S1JRv5I78V4ESa9PQv4WNZgh8g== ARC-Seal: i=1; s=201903; d=dkim.mimecast.com; t=1731604217; a=rsa-sha256; cv=none; b=jmDh8qKyRoks8kHsgiyfYUjC2xWw3gU8CgBbp3CYrpRyRJN74noQvsVBfYIttwuExNaqhh QypGZdT/ptSClGzKAoo1HloaNSyvmPvC50nOZLMeWT61dPMxU73+Q56G0mR4f68BRSiNeq s9N4p41PxkYjK0GVRwTdnTKcP1mt/wGdT60MyBsDzg0o2nbtUoLRan+JTVgXP6nvQl6sgq V09ZO5KCMbcUJgE8ZPgDPqiStAu6BYtcwfC0m9n6Z6Km3UFsiN+Sjzb6nuP9VqFjOL/hqt gOvtbIcJ17MgKUzURxoVQ0mhoE5jexpdasuT34uwb0Vw9GHiLuy6rtnJfJEi6g== ARC-Authentication-Results: i=1; relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=posteo.de header.s=2017 header.b=FDUV1xzm; dmarc=pass (policy=none) header.from=posteo.de; spf=pass (relay.mimecast.com: domain of felix.cherubini@posteo.de designates 185.67.36.66 as permitted sender) smtp.mailfrom=felix.cherubini@posteo.de Authentication-Results-Original: relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=posteo.de header.s=2017 header.b=FDUV1xzm; dmarc=pass (policy=none) header.from=posteo.de; spf=pass (relay.mimecast.com: domain of felix.cherubini@posteo.de designates 185.67.36.66 as permitted sender) smtp.mailfrom=felix.cherubini@posteo.de Received: from mout02.posteo.de (mout02.posteo.de [185.67.36.66]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id au-mta-58-5WtHhVLRNciyHYPpJuGNoQ-1; Fri, 15 Nov 2024 04:10:12 +1100 X-MC-Unique: 5WtHhVLRNciyHYPpJuGNoQ-1 X-Mimecast-MFC-AGG-ID: 5WtHhVLRNciyHYPpJuGNoQ Received: from submission (posteo.de [185.67.36.169]) by mout02.posteo.de (Postfix) with ESMTPS id 6A091240101 for ; Thu, 14 Nov 2024 18:10:06 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.de; s=2017; t=1731604207; bh=H4tPSAIedQx9Uw3laqeIq+D1yvp4F9f0l3+sxClBbS0=; h=Message-ID:Date:MIME-Version:To:From:Subject:Content-Type: Content-Transfer-Encoding:From; b=FDUV1xzmMIEs0cNZCqdBgkweMJtqkwRpwQK5FGDCy1kglkMPBixSqn+0RRbprFl5e UDDyTHhTZcYFg7JskmQZKvQEjnxB7A7FV5Uza8eIniVImrjDa5zolur6xwx3da1vPq WJDl1DNj2tS/Hn1ur77Vi5pLaBbSingvoMDTkCB6wGirnVD375ILebZzqjlg8K+Cul suH5SYkgFEvVrG7pA2Wa6hkvmyPs0DDPA9eYH49TP8gkI+wx+UMFxzrR/iXJlP3QZn nvx6rHOFgEiBYJN6RMvtZY3vkXZXC1+MguoBKvo/I7WSXng+U3pSIxTTdXIJa/xh6K 3O4jNfzL2bIag== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4Xq68t3Hc9z9rxF for ; Thu, 14 Nov 2024 18:10:06 +0100 (CET) Message-ID: <5c87cb8b-06c2-4fb1-9017-c7e2e47dcc3e@posteo.de> Date: Thu, 14 Nov 2024 17:10:05 +0000 MIME-Version: 1.0 To: categories@mq.edu.au From: Felix Cherubini Subject: Workshop on Homotopy Type Theory and Univalent Foundations X-Mimecast-Spam-Score: 0 X-Mimecast-MFC-PROC-ID: QLi280Hn012r_sTWW7ngDi8HHXLhhoeU0kBmgEhIu0s_1731604209 X-Mimecast-Impersonation-Protect: Policy=MQ - Tag Header Only on Default Settings;Similar Internal Domain=false;Similar Monitored External Domain=false;Custom External Domain=false;Mimecast External Domain=false;Newly Observed Domain=false;Internal User Name=false;Custom Display Name List=false;Reply-to Address Mismatch=false;Targeted Threat Dictionary=false;Mimecast Threat Dictionary=false;Custom Threat Dictionary=false Content-Type: multipart/alternative; boundary="MCBoundary=_12411150410160161" X-EOPAttributedMessage: 0 X-EOPTenantAttributedMessage: 82c514c1-a717-4087-be06-d40d2070ad52:0 X-MS-Exchange-SkipListedInternetSender: ip=[185.67.36.66];domain=mout02.posteo.de X-MS-Exchange-ExternalOriginalInternetSender: ip=[185.67.36.66];domain=mout02.posteo.de X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: SY1PEPF000066C3:EE_|ME3PR01MB6120:EE_|SY7PR01MB8286:EE_|SYZPR01MB7687:EE_ X-MS-Office365-Filtering-Correlation-Id: 8f56808f-a178-4778-0562-08dd04cf36b3 X-Moderation-Data: 11/14/2024 6:54:42 PM X-LD-Processed: 82c514c1-a717-4087-be06-d40d2070ad52,ExtAddr,ExtAddr X-Auto-Response-Suppress: DR, OOF, AutoReply X-MS-Exchange-CrossTenant-Network-Message-Id: 8f56808f-a178-4778-0562-08dd04cf36b3 X-MS-Exchange-CrossTenant-Id: 82c514c1-a717-4087-be06-d40d2070ad52 X-MS-Exchange-CrossTenant-AuthSource: SY1PEPF000066C3.ausprd01.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Anonymous X-MS-Exchange-CrossTenant-FromEntityHeader: Internet X-MS-Exchange-CrossTenant-OriginalArrivalTime: 14 Nov 2024 18:54:43.2495 (UTC) X-MS-Exchange-Transport-CrossTenantHeadersStamped: SYZPR01MB7687 X-MS-Exchange-UnifiedGroup-DisplayName: Categories mailing list X-MS-Exchange-UnifiedGroup-Address: categories@mq.edu.au X-MS-Exchange-UnifiedGroup-MailboxGuid: 9c2f954e-92a7-451b-b723-a07075d7adb5 X-MS-Exchange-UnifiedGroup-CustomizedMessage: RedeemedBusinessGuests X-MS-Exchange-Parent-Message-Id: <5c87cb8b-06c2-4fb1-9017-c7e2e47dcc3e@posteo.de> Auto-Submitted: auto-generated X-MS-Exchange-Generated-Message-Source: Throttled Fork Delivery Agent X-OriginatorOrg: mq.edu.au --MCBoundary=_12411150410160161 Content-Language: en-US Content-Type: text/plain; charset="utf-8"; format=flowed 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 1ST 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 * Bastiaan Cnossen (University of Regensburg, Germany) * Ambrus Kaposi (E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Hungary) * TBA =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) You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | = Learn more about Microsoft 365 Groups --MCBoundary=_12411150410160161 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=UTF-8 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D
1ST 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

* Bastiaan Cnossen (University of Regensburg, Germany)
* Ambrus Kaposi (E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Hungary)
* TBA

=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)
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
View group files   |   Leav= e group   |&n= bsp;  Learn more about Microsoft 365 Groups
 
--MCBoundary=_12411150410160161--