coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations

From: Daniel Gratzer <gratzer AT cs.au.dk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations
Date: Fri, 20 Dec 2024 00:40:34 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cs.au.dk; dmarc=pass action=none header.from=cs.au.dk; dkim=pass header.d=cs.au.dk; arc=none
Arc-message-signature: i=1; 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=Mss2DI1GIB4nFWVw0gf6e/KT8TPLMC+3rNPUZ8spxWg=; b=oWfyScCY3gVmzW3DtPMdtk+BDChCLUeNpI4GUlj/MKv9KTt3ImHHre1IHdHuEQZpl2aXnfRZXmB4HdD8zR3Rg95gs1htywwl1mLFnzlnYsQ4Dx6J2BMk3z/VIsmVYHGe/S1cJ5UG76aUcyeL4mzcA5hVsuBgMnARbWpj2fwVEouS3n4uyaEwBRd2Zujl0UD6RCmPxuSbbII1GHdP++iBn+eml6DMr0Ly8FiQXwza4kp9oJFToLXGvu+psymjg6Hb9+2P3OHYk3/mKxRoAxbN6fAJOmd9wXUlmcOymZRi1Te2YvZ705rChMIj1k0u25cAS05h6miHpnCW3Q0eVA+yfA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=qpmHd+9ZrRsLg0b7kdcOZ9dZvJn2ik30CT8SMmDRqireFoQMn7cXVpovMYVVjm01rkXO7T2HABcgkZX30C0Rr2VP88FGum0LgiUSih8aKNYySilaP9cBREtW77Yi9S4HcZ/dsnKBUpTyEV2nEtsmuXYPqKJtuO5pg8GWr+/fFtGUeaKNkh8Tnyh9lwAsvXzHkVURxVuy0iYlDPrbzoMMFq7xPFWuqj/H76cIhIWlVAFrD2b4sOSxCvrBQep4BwcMsmHDtiZEhpRNsRrGBUZgZssftDilEM88sqfzz+ebVLe8C5hpscfcHrP1bCl3Su2th7xYNV4fhLXuFLOfdrLGEQ==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gratzer AT cs.au.dk; spf=Pass smtp.mailfrom=gratzer AT cs.au.dk; spf=Pass smtp.helo=postmaster AT DB3PR0202CU003.outbound.protection.outlook.com
Ironport-data: A9a23:8NL1Ua4hs+iX2gZ7ySVSMQxRtCHMchMFZxGqfqrLsTDasY5as4F+v mEXXD+BbPiJYGPzco10ad6w9koP6MfUyYQwHgpo/iA1Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgtaAr414rZ8Ekz5a6r6WtD1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/hPB3EOAJ8jw7xIH18X6 fNFJx4TPynW0opawJrjIgVtrugJd/HRZNlH4FpdlWmCS/E7XZrEXqPGo8dC2ys9jdxPGvCYY NcFbT1ob1LLZBgn1lU/Vch4xb/xwCeiNWIHwL6WjfJfD2z7wxZ4zKrgKvLeYZqDWINZnS50o 0qcpzygXUhKbYL3JTyt11GXnqjlxT7ABsEMG6LgzMdzmAWT2TlGYPERfQDg+6Xm4qKkYPpUL FVR8S4zp4Ap5UmzR5/8WQe5qTiKpHYht8F4FuQ77ESLzbDI4wuEHG8cQzdTb9p/7ZdsHGR1i RmOgs/jAiFpvPuNU3WB+7yIrDS0fy8IMWsFYixCRgwAizX+nG0tph/uReZbLbyOt4fKBw+p3 z/XowYg1oxG2KbnyJ6H1VzAhjutoL3AQQg0+hjbUwqZAuVRNN/Ni2uAuQiz0BpQELt1WGVtq 1AltqCjAA0mCJiMkGmLR/8RHLy0/fGdPTTOhlg2RsF7rmzypDikYJxa5yx4KAFxKMEYdDT1Y UjV/wRM+JtUO3jsZqhyC25QNyjI5fawfTgGfqmOBjarXnSXXFPalM2JTRLNt10BaGB2zckC1 W6zKK5A90oyB6V91yaRTOwAy7ItzS1W7TqMHsyllE/9jOTGOyf9pVI53L2mPrFRAESs8FS9z jqjH5Xbk0o3vBDWPneIrNZPcwxiwYYTWcip+pUIHgJ8HuaWMDp6UaOOqV/QU4lklL5SjeDG4 jm2XVVAoGcTdlWWQThmnktLMeu1Nb4m9SJTFXV1YT6AhSJ/Ca7xt/13X8VsItEaGBlLl6cco w8tIZ/YWqwnp/Wu02h1UKQRW6Q4K0/32F/XYnH+CNX9FrY5LzH0FhbfVlOH3EEz4uCf7KPSe pX5jliDE6kQDR9vFtjXY/+Jxla89ypV0uFrUkeCZpEZdEzw+cI4Y2b8n90mEfEqcB/j/zq90 xrJIBE6oeKWnZQ53uOUjo+5rqCoMdBEIGxkI0fh442bCwzm70u44IoZUO+3bTHXD2z136O5Z NRq9fL3MdxZvVVwmK8lOY1O4YMhwtjJmZp25xZAGSSSY3uJFL9ff3qi2+NevPZ3wo4CgxO8A B6S8IJkYb+mad3sAQMTLlB9b8Co9/Idqh/N59sbfWT44y5W+uKccENwZhOjtg1UHIFXAqgEn 9gzmZcxwBOtrzYXKfOEgTJw21XXC0cfQoM1sp0+K636uDoBk11tT8TVNX7r3cupdd5JDHgPH haVo6jn3JF32UvIdisIJ0jnhOZyq8wHh0FX8QUkOV+Mp9vig8031j139RAcbFxc7jdD4tJJF llbDW9HDoTQwG4wn+lGZX6mJC9ZDh7A+kDR9UoApFeEc2aWDF7yPE8PEsfT2nsG8lBsXClRp 5CZ72fHbQzEXu/M2gkKZEo0jMC7EPJQ8FXZldGFDva1OcAwQQDYj5+EYUsKrBraAv0NunDXm NkywsFObfzUCC1BhYw6FIiQ6poIQj+mOmFpYK9s7YEJL07maRCw3jm/cGWsS/NwOs7l6k6cI O5tL/JpSB6R+nuvrDcaJKhUOJ5yvqcjy+Qjc4PRB1wtkuWgvAsylanP5w7ChGMPaPd/o/YXc 4/+WWqLLT2NuCFyhWTIkvhhBkO5Rts1PCvHw+G/9bQyJaIp6e1DXxk77eqpgi+zLgBiwhOzu THDbY/wy8hJ69xlv6noI5V5KzSEE/HBf8XWz1nrqPVLV83FDunWvQBMqlXHARVfDYFMZ/tJz 4ayoPzF92Kbmo0pUlLpuYiLTIhIwsSQYNB5EOzKKFtioC/Tf/O0vjUi/TijJI1rgeFtwJCtZ zGFZfuacf8XXNZgx0NpVRVOLiZFC4nKavbPmCDsidWNFRkX7iLfJvyF63LCTD9WZw0ICbLEG y72vPefvfVFnbRxGS0rHPBCKL17KW/FRqEJWYDQtz6ZL2/wmXKEmOLouiQB4AHxKEuvMZjF8 6OeYyPhZTKOuK3s5/NIgbxY5xE4Ii50vrgtQxg75dVztQGfMEcHCuYsabM9FZBel33J5qHSP T3iQjMrNnTgYG5ibx753dXEWzWfDMwoPvPSBGQg32GQWheMKLKwOplT3QY+3C4uYRrm9v+tF v8G8H6pPhSR/IBgddxO2tOF29VY1tHo7VNW33vikv7CIQcUWpQL831DIDBjdwL6F+P1qUGaA lRtGE5lRhi3R3ekRIwkMzRQFQoCtTzi8yQwYG3diJzDsoGc16tbxOe5J+j31aYZYd8XIKIVA 0n6XHaJ/3vcz0l7VXHFYD71qfQc5TO38smGwGvLaSdJp5vosDx9FP5axXFJS9w+8glCFV+bj iOr/3U1GEWCLgZWxaGSzgIKvZl2VxrgyhnX2RXnq2aufQMRlrDkl9qClWoX6q0cb4DopANRX XEeby59ZnWI4SD8q2AWWusz/zS67AJ4KZUAeiszCJrv1BuvIIOY+HaNzGliv+9sHLZ4Kkm4u UpfPxjROG5qY89X4z3ZoQ==
Ironport-hdrordr: A9a23:lZKPwa8OT7gMFLucgKBuk+FGdb1zdoMgy1knxilNoENuH/Bwxv rFoB1E73TJYW4qKRcdcKO7SdC9qBLnhOhICOwqUYtKMzOW3FdAQLsC0WKA+UyoJ8SdzJ876U 4IScEXZ7PN5DNB/KXHCXyDYrMdKa68gcKVbInlr0tFfEVPUeVN/g15AgGUHgldXw9dH6c0E5 Ka+45uuyegUW5/VLXxOlA1G8z44/HbnpPvZhALQzQ97hOVsD+u4LnmVzCFwxYlVS9Vy7tKyx mOr+W53NTvjxiI8G6S64bh1eUZpDIn8KoDOCW4sLlYFtwrsHfpWG0uYczAgNl/mpDW1L9jqq i2n/5nBbU615qZRBDJnfPgtjOQqgoG+jvsz0SVjmDkptG8TDUmC9BZjYYcaRfB7VE81esMpZ 6j8ljpxKa/Nymw7hjV9pzNTVVnh0C0qX0tnaoaiGFeS5IXbPtUoZYE9E1YHZ8cFGaigbpXZ9 VGHYXZ/rJbYFmaZ3fWsi1mx8GtRG06GlODTlIZssKY3jBKlDRyzlcexsYYgnAcnahNP6Vs9q DBKOBlhbtORsgZYeZ0A/oAW9K+DijXTRfFIAupUCTa/WE8SgPwQrLMkcsIDbuRCeA1JbMJ6e v8bG8=
Ironport-phdr: A9a23:jKhTnR0zEyyrBLNSsmDOXwwyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeGo6w11RSTBs3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pDdfglEniexba9vI Bm5swncuNQdjJd/JKo21hbGrXxEdvhMy29vOVydgQv36N2q/J5k/SRQuvYh+NBFXK7nYak2T qFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4 qx2RhLklDsLOjgk+27Ql8JwkblboAq/qBNj347aboaVNP9kcaPce9MRWG5NU8lVWiBEBI63c okBAPcbPetAr4fzuUYArQewCwevGOzgxSRFiWXq0aEmyektDR3K0QwmEtkTsHrUttL1NKIKX O671qbIyzTDYO1S2Tzg6YbIaAouoe2NXL1ua8ra1E4iFwzfjlqKtYzkPi2a1v4WvmeH9OpsT /igi3M9pw5soTii38EhgZTGiYwJ0F7L7zl5wJorKt2iTk52ed2pHZlfuSyeOYV7XN4vT39pt Ss4yrMLt5y2cicJxZg62hPRa+CKfpWH7xzjVOufISl0iXxmdb6ihxu+7EytxOP6W8Kp3lhKq S9FncPNtnALzxHT5cmHSud9/ke8wjmDzQHT6uZcLU8qj6XbMJ4gzaIwlpUJsETDBDX6mELsj K+ZcEgv5+um6/z/b7jmuJOQLZJ4hh3jPqg0m8GyAf40PwoMUmSD5+ix1aHv8EP8TblXkvE5i KjUvZXEKcgHvaG0BhFZ34k55Bu6CjqqzskUkH8aJ19bfBKHkpPpO03QL/DiEPm/glWtnylzy vzaOLDqH4/DIWLZkLj7eLZw805cxxQ3zdBY/59aBKwMLfzpVEHtqNDUEAM1PxKqzunpFNlxy o0TVXiIAq+ELKPdqliI5v8pI+aRfoMVoCz9K/855/HwkXA5hV4dfa6v3ZcNb3C4A+hmI0GeY XrrgdcNC3sFvg07TODyiV2CVyBcZ2qqUq88+D03Ep+qAZveSoy3gbGM3D23E59Ua2xeD1CDC 3bod4GKW/cWbyKSJ9dskjMeVbe7V48g1A+htBXhxrV7NerY4DcXtY/52Ndo5O3fjRcy+idsA MSHz26NV310nn8PRzIuwaxzuVZ9xUub0ahkn/xYEsRe6O9OUgcjLJLT0+h6C83pVQ/aZdeIS FOmQs28Dj0rT9IxxcUOY0dnFNm4gBDDxXniP7hA3beMHdk/9r/W93n3Pcd0jXjcnuF1hF4/B 8BLKGeOh6hl9gGVCZSfwGuDkKP/Wa0a3SPJvEiZxHacsVsQBAFqWLnXUGo3bVCQpMm/6kCUH OzmMqguLgYUkZ3KEaBNcNC80QQurJbLPd3fZzj0gGKsHVOSwbjKaoP2emIb1SGbCU4ekglV8 2zVfRMmCHKHpGTTRCdrCUqpe1nlpOZkoW+pQ1UcxBrMZlAn27nmsgUNi6mkQugIlqkBpD9nr jx1GFin2NeDBMCJuxhsZo1XepU0/RFL1jGRrBRza6SpNLsqnVsCa0J3skfpgg1wEZlFmNM2o WkC4CApEZjAigsbXA7Ahcu2PaDLIG7v+hzpc7TRxlzVzNeR/OEI9eg8rFLg+gquEyLO6l1B1 N9YmzuZ75TOVk8JVI7pF1ww/F58rq3bZS8048XV02dtOO+6qG2K3dVhH+Yjxhu6GrUXeKqZC A//FdEbDMmyOaQrnVaudBcNIOFV8uY9Icqnc/KM3KPjMvxnmXqqimFO4YY11UzplWI0RfTBw 4QI2dmTxU2OSnHwjxbps8z6n5xFeSBHBnC2mmDvAI9cYLE3fJ5eVD3oepXugIsjwcGyCBs6v Ba5ClgL2dGkY0+XZl35h0hL0FgP5Gagkm2+xiB1lDcgquye2jbPyqLsbkliWCYDSW98gFPrO YXxgcodWR3iYBIgiAmo/27x3O5SueJzLCOAJCUANzizNGxkXqaq4/CNecdT+p4ymS5MFu2hJ 1yZAO21s14R1CXtGHFbzTYwemSxu5n3qBd9jXqUMHd5qHexldhY/R7E/5ScQPdQ2mBDXyxkk XzNAVP6OdC1/NKSnpOFs+akVmvnWIcBOSXsyIqBsmO86wgISVWwhfmviND9OQMhlybmkdVpH SnFtxfzZID32r/ybLghJxExQgGhrZUlUohl2pM9npQRxWQXit2O8HwLnH2yVLcTkaPyYXwRR CIaltvc4QzrwkpmfTqCw4P0UGnYw9M0OoP8OztPnHxgqZ8VW8L2pPRekCB4o0S1t1fUaPl5x HIGzOc2rWQdiKcPsRYsySOUBvYTG1NZNGrijUftjZj2oaNJaWKoabX12lB5mIXrA6uLvhNRQ l7yYdErAGl87Y8sVTCEmG228YzidNTKOJgcrBSIgRrap+NObpss0PYJz3kvKSf2unsrzPQ+h Bpl0MShvYSJHG5q+bqwHh9SMjCmAqFbsiGol6tVmdyampy+Bpg0UCteR4PmFLj7WCJXr/nsM ByCVSExumvOU6SKBheRsSIE5zrOC8z5aynRdSNflZM6A0DAbE1H3FJIBHNjxsF/Tkbyg5W/O EZhumJMvBih8kMKkqQwcECiNwWX7AawNmVpEt7GdEAQtkcaoB6Lec2GsrAuRWcBpsbn9ErVb TXELwVQUTNQAhDCWw+lZv/2ooCflorQTuumcamUaO3X+7UHDqWGmcr3gNkho2bEN93RbCNrV 6RpgxMaD34lQ5+LyXJTGkl132rMd5DJ/h7ko38u95nt/qizA1C/vdPXWekVbIwn+gjo0/2Kb 7fC3X8gezgEjshezieQkOpNmwNL7kMmPzi1T+ZavHaUHvuJw/1ZU0ZAOS0rbJMaveVhhEEIM MrfwLsZz5ZAh+UuQxdAXF3lwISyYNASZnu6PxXBDVqKM7KPIXvKxdv2aOWyU+8YgOJRvhy28 TGVdi2rdiyEjCXsXguzPPtkoAvABCYG4tnnWSs1UTOlS8/6YBqmNtMxlScx3bA/mnLNMygbL CR4dERO6LaX6EY6yr1zFndA4XxsMeSf03vDqbCAc9BI7L00XWx9jKpC7W4/yqdJ4S0MX/Fzl CbI75Zvr1ygjuiT229nXR5J+VMpzMqAuURvP7mc94EVBCyCpUpUqzvNTUtV9L4HQpX1tqtdy 8bCjvf2ITZGqZfP+NcEQtLTI4SBOWYgNhzgHHjVChEERHilLzK65QQVnfeM+3mStpV/pILrn c9ERaVSSE44DNsREQJsAZoOI90kO1Fs2a7el8MO6Xek+VPJQ95Gu5ncSv+IKdnFcw6j1eMcP TA1meuja4MOKof8xkpuLEFgm5jHEFbRWtYLpTB9aggzowNG9300HQhRkwr1Lwiq5nEUD/u9m BU73xB/beoa/zDp+14rJ1DOqXh4gAwrlN7imzzUbC/pIfL6Q9RNEySt/RtUUNuzU0NvYAa1h 0AhKDrUW+cbke57bW4ywA7E5ckTQbgNF+scJkdXnKzfZu10gwgE7Hz/mgkfo7OCUMUH9kNic Ibw/S8anVs7NJhtY/SXffcBz0AM1P/U+HbwjKZphldZfhhF8XvOKnNS/hVQbf9+YXLvp7MJi 0TKmiMfKjFUC7x2/bQysBt6YrvIzjq+geRKchnjbrXGfa3F4zCSx4nUEjZSngsJjxcXp7Eui JV6KhPGWRx3l+nDUEhYfcvad1MPZpILpiGKJHSA7b2Wk8ItZ93vRKe1FIrs/O4Vmhz2Rg9xR tZVt51TEMX0ixPTdZ+/fuxClExl5Ry1dg+MVK0bIUvSwjlb+5rtwscvhdsPYWxHSSB0NSH9j l44jgQxxvOeGts1MC5ytm4sPWlwUdD8ly0L5xyo7RGb+Lkh8lDYt2XXm3yIV3/7csZpY+qSa VV0Etaq9D4j8q+wz1nK7pHZIGK8PtNn6Ian1A==
Ironport-sdr: 6764bd05_HGgYMTIGA6BkPTbinMAsUlwj8BvUkSGaY0R0rOGJONeXyoL Pe0SCFpaHgh//cBae8ryRXjJMkQBnkWlDwlMI8Q==
Msip_labels:

Apologies for any duplicated messages.

==========================================================

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)

------------------------------------------------------------------------

Workshop on Homotopy Type Theory and Univalent Foundations

15–16 April 2025, Genoa, Italy

https://hott-uf.github.io/2025/

------------------------------------------------------------------------

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.

================

# Invited speakers

* Reid Barton (Carnegie Mellon University, USA)

* Bastiaan Cnossen (University of Regensburg, Germany)

* Ambrus Kaposi (Eötvös Loránd University, Hungary)

================

# 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=hottuf2025.

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.

[Coq-Club] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations, Daniel Gratzer, 12/20/2024