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 autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-pj1-x1040.google.com (mail-pj1-x1040.google.com [IPv6:2607:f8b0:4864:20::1040]) by inbox.vuxu.org (Postfix) with ESMTP id DA3852405A for ; Wed, 15 Jan 2025 19:30:54 +0100 (CET) Received: by mail-pj1-x1040.google.com with SMTP id 98e67ed59e1d1-2ef114d8346sf264366a91.0 for ; Wed, 15 Jan 2025 10:30:54 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1736965852; cv=pass; d=google.com; s=arc-20240605; b=RJcU5NN5843EBj1yxSTDCng3939wWIz5PuawZDu/nVCcKyk1xFd0XRPKGVT4bpJBmd Is912/Kup+PA5YuQdwVvroHRdh2eGrEjPBBz2M+oGYx2fEhOrvleRbT2OkGqA5Z6LP/T 8BqXkolMhAflXYFcSoKr9NqrQNM5bksjjqJcJ+rff9jG7EIyHoyae9GO2tVzCOYIobFb /cK2XRum98hpirsEql6k3JUtT6jYpHZKm8eeSevG6ScY+MqLtlt8vrCyMltDzPblpHw3 nL84yl8urnLC1L4FZ1V7mjfJeKLN7zO82p2PQ4qq4PXiscLCOFyrQv+lSmHvO32czx+k rz/g== 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=tN1V0VWDstQt4TODJeX1zU1+/WHoKHzMVb1G0UeHRYo=; fh=8eFzt+xUCrjqEUCNBjnjgLGeJWBuwknEkbUtknJbmhc=; b=XQUOwMuIQpp8Xxkh8ErXwhFGftCSWoI0qr87PYC4b9d5198UoFMvDRtH/B8f3dsXiN Apgzk8WAvV8KryGakRk4uDRtulI8wihvqiVGHxrVMvwFSE4hS/Dj1ZZCWvDQa9SbDuXS DixH+BORrkkkmKhZ5cofAWAFPr4Yje8Zdr+GylEpV20HBG/HY+X891JTN+aD/bO3HncP UJmo9+5fmO2mGMiiIGqp0MhJo6r2QQ6czuY+aCIomaj7QJeQdjfXMtGlsFPPyw1WH5zr sdzdXV3COdxcMZ0enGatR7Vw3HVt5n8SIffMzAC7BR/M7g+udnNC9jBbQho3PKeXOGYf am9g==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=e+2bT9xF; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b34 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=1736965852; x=1737570652; 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=tN1V0VWDstQt4TODJeX1zU1+/WHoKHzMVb1G0UeHRYo=; b=Au2FzfrUZ9TpmTzraBZFczuKw15EIiAFjfiaXWHStOz1RGDM8KTakP4VLcuc3mUeVW UdAeqn8WWZ3LtMLxXVd7rdBEq8sjIk0uwMwQ1PYGl/4Twepps6s+JNcLLFnEMXQ9VRRd cznhvl8nKIg/rxeWuL91ghSFJF72WVWzbv0D8+Aqa6gf41ptNEl/gAQqUN1Pc0N5GpAA 8IEchM99Xrru1NdCbtL9zz9V9pzvLVnJKbjELU9VGX7tTn2mXLkOqnUBxs25W52OazDP BTFAn17GiPhEJAbq6927lYOK4Q2SuyX5HQkOk4P5/yzPHxuBZeFUB/I5UJ1dx2KiT/YB yuyQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1736965852; x=1737570652; 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=tN1V0VWDstQt4TODJeX1zU1+/WHoKHzMVb1G0UeHRYo=; b=Y31SjR1uq/dq3MzRTEWF42KhQy7HG8WL9E8tjcquYANzZ9QbWP0gE9wvHiX2RgzuGp 5pxJzNqDy1uUs4ccX8IZeCVw6pZREv46VwH7S0VHqhrO98ntRDg3jNxt9mznyTdiny7L NF0Zy7dsVD6iFYG6HJEQRJsMbelYG5B2OVXm6EFLHKFxqVrWEeMv0tFTN3ZkRbSx5uaE VPUNTph7Lj1hEVQ/hT/Lm9TSdFQ4tyadeBrpxde6RJkUCRoIbC7q0qrlyfGtUBLQVOFJ CLNQiKDACecLED+BpvtULQs5RuGs6l6x6aW/XSpxsK5ZbVGGIhulcLja/TjHStH9290f Lo4w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1736965852; x=1737570652; 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=tN1V0VWDstQt4TODJeX1zU1+/WHoKHzMVb1G0UeHRYo=; b=c6cCRxAWHamyXJYdYneBibLqqSlF2Ws6RCmb9g88jnw2IEiLM0tBNuvFEcfb90fZ0M hxvV9dFv4xBtuHkDDrddzIGBAvDWcebQSld+B+kVh54hZXPBmeLwg+B64Iq4VX+jixkV 6tOnhDZ4KXA7Im9mXUIlXjG1V/BOqKOl5uLuAtzvlMaYMwojZ47tDrsSQx2AMuISxugF UuEt2Hhs5as38VlHlztac9rqDRsnWkWcOraWn69c0j2X3qXwn4lH4WkrAlglzRj2Zk9E tK3prqD1QoGmuWB+ByZO2mKUeDDFwfR3aiTRXp/NmnXHoycI2Yai7SPgFpatyPe6AN3f FnNQ== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCUKPoTe+0VFZB4MYhX2O9RoubZiG+FdOADGN5wYbYVUKLTzBSQFuc+3dY2r21P6PtPG6Q==@inbox.vuxu.org X-Gm-Message-State: AOJu0YzjXFC9iBV6czWnbGTa5nSSyK3qapJ17UoXp3M0OXmzkjkE9W77 s4dWnzAYYS1+RITev4tGDCmf5kswAIJujoi+WTWUaVk0cTx0rSBd X-Google-Smtp-Source: AGHT+IFGlFE3LKwEjydIQT26qfiaOWa2pB3gouGnZYBTnVu9sRuRGBGQlBP4Dxinj5GIA2QuvjoIJw== X-Received: by 2002:a17:90b:3904:b0:2ee:a76a:820 with SMTP id 98e67ed59e1d1-2f548f6a857mr48444680a91.18.1736965852062; Wed, 15 Jan 2025 10:30:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90b:274d:b0:2ef:9dbc:38e5 with SMTP id 98e67ed59e1d1-2f74c94aa18ls137813a91.0.-pod-prod-02-us; Wed, 15 Jan 2025 10:30:48 -0800 (PST) X-Received: by 2002:a17:90b:4d10:b0:2ee:cd83:8fe7 with SMTP id 98e67ed59e1d1-2f5490edb9emr42873084a91.35.1736965847979; Wed, 15 Jan 2025 10:30:47 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1736965847; cv=none; d=google.com; s=arc-20240605; b=layoLeXEppkiJx1oHc0M6qv4tseXHnNhZo3FNilFQqfcT57YChhlfksJlk/edCXtfB /V5IxtbYfNkWyxgWd6ldGUaNjVnl3nVoZZw4b/YvSKiQseHB8l2S+OYI8u2/bzvcSRh2 MTuHDJf7kbLKWnWIKvOnBC99sQk/DqqRy+1wRdUANixpaEj2dPNCUnjBsUgl9EItp06O JsBkIxM88ha9TvAhT/sjNQjVDnicmpMBW33n0aZKxwTh3xlUMfC+Skbs9uTkQ3JOmyq5 ehFOvgNdBhYFK/A2sN0su/hCe7DqhBZ0tvpD2LdGebg56An0+y9n9sBdjXosOw9Uz706 NPhg== 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=sQbbXH20P17I77rO6uopoGNSdFVWZegiWL1jCAXblzc=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=Ld3/s/txOnYE9Dl8RzfGWjTUliGB5U22W9pZoDDGdshnNqPeO5DLD0x3solTpr4Toa BKFH7AwOJB07f+y/BnppBjGhf6mdq614G/gBBITBdB9AErB+OKmTn9NCmaR8WWygQUok N/tzCiuUqvjcR3rOONL0FiiqG7nD1zHexuMsxAhnXR3J3Xs1Pk1jz0Pzz+iVzFZpfCiU vaHvSx1k0EpoiTa60dULRrZmov4DLlNIFRmrZjIPhWErVEPxxjovR9FaDptOMDqzEOTQ J3xBzgl98+BaZiOwxBeIelVZgNmuBOiEbMIC3io2ayUaLiwv3XxXvXgIuSMjKb+DkxjY Cr4A==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=e+2bT9xF; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b34 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-xb34.google.com (mail-yb1-xb34.google.com. [2607:f8b0:4864:20::b34]) by gmr-mx.google.com with ESMTPS id 98e67ed59e1d1-2f72c14fcebsi88587a91.1.2025.01.15.10.30.47 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 15 Jan 2025 10:30:47 -0800 (PST) Received-SPF: pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) client-ip=2607:f8b0:4864:20::b34; Received: by mail-yb1-xb34.google.com with SMTP id 3f1490d57ef6-e3c9ec344efso71064276.2 for ; Wed, 15 Jan 2025 10:30:47 -0800 (PST) X-Gm-Gg: ASbGncs4ZYvf2Xq7LopBLtu7KkQKGKNCCrAHVRqRz1t8eO6z/mteYK1AT4417e3oyit WsBtKPq9BQ+D6GX+tRbn+wkBdZJIjYgbTJ4M= X-Received: by 2002:a05:6902:1146:b0:e57:4688:4042 with SMTP id 3f1490d57ef6-e57468841b4mr12340847276.13.1736965846307; Wed, 15 Jan 2025 10:30:46 -0800 (PST) MIME-Version: 1.0 From: Daniel Gratzer Date: Wed, 15 Jan 2025 19:30:10 +0100 X-Gm-Features: AbW1kvYgdWk-aXTbyuO6jg2EkzHHi2Q1Dt3M1JRV8SOOlqmvLrT_EC1b5tGiuS8 Message-ID: Subject: [HoTT] Final CfP for HoTT/UF 2025 To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000419b20062bc2e094" 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=e+2bT9xF; spf=pass (google.com: domain of danny.gratzer@gmail.com designates 2607:f8b0:4864:20::b34 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: , --000000000000419b20062bc2e094 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 FINAL 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 ------------------------------------------------------------------------ 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. --=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/CACbeAXAY8yZz%3DZdZcrrWY-5MzGHw%3DkJEVpN97c3OABU7MjpJTQ%40mail.gmai= l.com. --000000000000419b20062bc2e094 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
FINAL CALL FOR CONTRIBUTIONS AND PARTICIPATION
Workshop = on Homotopy Type Theory and Univalent Foundations
(HoTT/UF 2025, co-loca= ted 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

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

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 ho= motopy theory. Univalent Foundations are foundations of mathematics based o= n the homotopical interpretation of type theory.

The goal of this wo= rkshop is to bring together researchers interested in all aspects of Homoto= py Type Theory/Univalent Foundations: from the study of syntax and semantic= s of type theory to practical formalization in proof assistants based on un= ivalent type theory.

The workshop will be held in person with suppor= t 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)
<= br>=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 enco= urage authors to include information of pedagogical value in their abstract= , such as motivation and context of their work.

--
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.goo= gle.com/d/msgid/HomotopyTypeTheory/CACbeAXAY8yZz%3DZdZcrrWY-5MzGHw%3DkJEVpN= 97c3OABU7MjpJTQ%40mail.gmail.com.
--000000000000419b20062bc2e094--