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.9 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-x103f.google.com (mail-pj1-x103f.google.com [IPv6:2607:f8b0:4864:20::103f]) by inbox.vuxu.org (Postfix) with ESMTP id 037802841C for ; Thu, 26 Sep 2024 16:22:45 +0200 (CEST) Received: by mail-pj1-x103f.google.com with SMTP id 98e67ed59e1d1-2db470aa646sf1063999a91.3 for ; Thu, 26 Sep 2024 07:22:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1727360563; cv=pass; d=google.com; s=arc-20240605; b=aPBlehy2Gtx9V4G5cOKDKnZSwh/smpD1ojyHOb3SPlnGQlGm1aJwStb57CiWNpqoMw TxgIgGm/mlJNAakS0OKPb8nH39Eapgdht1+R0wxNOxalwh372eN5eLeNk3kHPGGTgo9j HhxMHd0fNc6qWpqD/gvO5XpV0IJmycFz12sf2KVogz2+cIHiqriruyZt1yh3ESDzsNAf AGObE9Ow1JwJvR/FZJdt0nzv6AuMl0QsnZasqNTYlpfXPCkVXE1526FlHAe9vfOOkOPX y9hyDYTXH0EDoPZDiW8xMIV0eLy+0ij5PJkpeEmXXHYshISMS2JUiZqE2mYiL7U/vrDl 83rw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; 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=ZC9dias/FTkKDNuootbasrRS0NCz5hfKPEaYs5bJyiQ=; fh=BYP5EF4gi7M8GwYoMR6Caq7J8O/o5hq7pk11ADisqhY=; b=KKBvDkythJndJq3ojLcXMYQkLIoTCnUip4iUvnulFURWRCr8Ol7YD98595v+10jeNV WXugRjetA+rElbWX8zat3XMVnd6PLEn85PiOsRIPx1nF/wmsL/wIt8Fs9bPcIxG9+ghb TUApgDQXmh1iJHG3pnag7+WS8Rl5kOJHMcq5VS7RJyo33ALdzB+xV+//l82IOm9+l6tY Nfh8RbMpxbLFyYHX+ANcMoJzH0higpja4UoHBua+0UH8l6zKd5dN98RtO/QDqxo4xnFn 73t2iN25FwLQ4cEffZDo0OvTfQgwg4keMFMYDFMLvNzqX8qNJzUD5k6IXWwuRJdI0k9H xqUQ==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=lzAykFHu; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::732 as permitted sender) smtp.mailfrom=rmogelberg@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=1727360563; x=1727965363; 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=ZC9dias/FTkKDNuootbasrRS0NCz5hfKPEaYs5bJyiQ=; b=P9srq3SWna9p/xe5TOzmbsjs4ISn6JWaVV78NEabSVqqOBuFlKkrJtpyphiU23IsLt RE7kmSCh5YzUf2KA1INj216TQ0FQx88xnS/M6bbvFjcbchoTs8FYAv0kOGE+R18B0i3w oc3oQAbxutE9ty84/P8InZdLhnO5iQeBKhoW1sfkYzVObmXbNnpOiIJdl2hNcswrw7QB bVdp2ZaXvBjIQtWnRJfkPphmH59tgVrSk2H/hsrO/ddnNSiLXwldg0qozL9g+CZDKXRb +oooCUU3ukIr0cu1Ngq9R/6+ERI8G60mbq80F9cZS6SSEvls2Hyat7aqdrbkXyjxRDG3 eQxg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727360563; x=1727965363; 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=ZC9dias/FTkKDNuootbasrRS0NCz5hfKPEaYs5bJyiQ=; b=SzsXK/75YsO93Ag8TOwnBICkc2YenU9I4b1lwV/fyziE5VGzTF40LKkdm2qYYdp8rj LV2MjQVR7svuM2NqqV/gIQC7bSH+tlht8mwlNVZP2tMwNbkooO93Uob3OBukIX/8tkjS Aim1bluW5+e77Qf8nL8dsX8U6+aVy+EUsBOXfPaY0ZDQ1x81fudS6dfDi/guSCLMqmwj 1sgGCzMieao5ektPNv/N9GxyViphTaBP/c8j3xb2MmBa8oiZqeKIjPbCXzNIgV2hzP7M NRkXF7+AF+c+eXtsP0clujTezr6gJ4+PGiKUS4NRWMffMpN6MExqsHqGf0VzNDtG2MI7 hcyw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727360563; x=1727965363; 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=ZC9dias/FTkKDNuootbasrRS0NCz5hfKPEaYs5bJyiQ=; b=cketd8HtFGbcyc0kFgLlwvHuu02u6mfy47PDWB+iWS7mPdmnPP8kjX8QAItM+lEs37 lBJxE77lUQHNU68Uqxugc6WaWytOnU6gTxcSIxE8CbxZwh1Cch2Ve9mf9X1STK7VfBNZ KdU55tFb4z6Y7ceLmqouIm3/l6XndknvtwIfe6rBi4RUhmHHqdvHUyNJL2IVcXUrNrE+ Q+f2gmzwEYcuxbKJBJNIR0Sf3NE+XEJFC9PBj2q2Opfq5OJdVfALygwSCW/vhl8weBUl f7YGcZ98/rRPmF1z8zjtuLRIxA/8YbdWf9UZiggF7ATIEecGV3Av1KC3BEuUea6EiYsh T7qg== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCUOzQtrGRJmARTP9lpL4ew9sJkDyQVXT096CGEb9xfeJZ/Roaq2xM0NdHRHnIJrqDB28A==@inbox.vuxu.org X-Gm-Message-State: AOJu0Ywpcj8zXo+OlvK3oTxgz3T8UR/jICJrpG/ywwePKwuqlsRnRLUN vJjwwTp23kuv6q/Ux40gT/HXRnyVDk9rZTBC1ZyX0s0sECy5pBaS X-Google-Smtp-Source: AGHT+IH921GvZtZok5Ndk/NHW8h0bttYq9tT+FIkQRsc2eXNPM70oaLRk8++IWwylLYPaT3PYvV5+g== X-Received: by 2002:a17:90a:f09:b0:2c9:7e9d:8424 with SMTP id 98e67ed59e1d1-2e06afbdcd2mr7115351a91.30.1727360562919; Thu, 26 Sep 2024 07:22:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:eac7:b0:2e0:8b1c:34eb with SMTP id 98e67ed59e1d1-2e0908c38c1ls777417a91.0.-pod-prod-09-us; Thu, 26 Sep 2024 07:22:39 -0700 (PDT) X-Received: by 2002:a17:90a:f09:b0:2c9:7e9d:8424 with SMTP id 98e67ed59e1d1-2e06afbdcd2mr7115130a91.30.1727360559144; Thu, 26 Sep 2024 07:22:39 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1727360559; cv=none; d=google.com; s=arc-20240605; b=jCeiiMY4IEp275DOPH8+S9qz3pcewn6ood57NvP+LoR/ase1u1MmumPBfvErlXZgB+ c+1cX69tqO/cDEWLAF/GYwvAEQqvVcAYsDE52Gf5gbtPg5Lnjrs2noHE4nSNcBlB9UxA CVJ4BehdjiZRhbLvXM16taLXgSAYNx1shF3ZRmKcp4FgOpZBHEYkIzGnFJAXbA+yOLVW HpjVy6k2DYm3pd7qSA9yuZKSQubVc2CrWciqoySDb9xg5BR+X/l9I5CIW7G3SYG5wgxt Z/lbBqs2yioS0GfC7ksaKFxI377Zrm4Eq31n+akku8OtYK88fh/L72FuAiuGVQ2whn+T SarQ== 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=8UxXSjyZnoIKK/vQf9BkOtC+jZZjMCRb0eqWykQmcpo=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=g+ayeE/0b5WsOpV1BZ+afcRpySM36AEnC7PTJZdiskZnMJ9B7Zf+FL6mX5gTZtGhO+ qLMCh2wSO1UJq1ntYLTm4QvdCVYjx78YwcTZGxOZ8CzlV8AI/pZgOOnGeDpTKxjCibGb adLTOHBUV+5NWEIsQ0y3YJ+vn45vTP/7/1qhnVTyqI6XM8hzypoZ7Ko2tupF0q6jjW0a ICpNfL7vV9mKmOs9k/q7Zfq6GKZc42zFZRteLEhJ1tmp7xNlwtAEUppXnjNxcZU7YU13 4ENdhJQJ/v0RU1kPIT4wIs/LNe38Izqr6HeySZt6XYGfjZO5Qer7FGXD0yTsT4FT7RFx rR8g==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=lzAykFHu; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::732 as permitted sender) smtp.mailfrom=rmogelberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Received: from mail-qk1-x732.google.com (mail-qk1-x732.google.com. [2607:f8b0:4864:20::732]) by gmr-mx.google.com with ESMTPS id 98e67ed59e1d1-2e06e2b622bsi145259a91.2.2024.09.26.07.22.39 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 26 Sep 2024 07:22:39 -0700 (PDT) Received-SPF: pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::732 as permitted sender) client-ip=2607:f8b0:4864:20::732; Received: by mail-qk1-x732.google.com with SMTP id af79cd13be357-7a9ad15d11bso90689285a.0 for ; Thu, 26 Sep 2024 07:22:39 -0700 (PDT) X-Received: by 2002:a05:6214:33c9:b0:6c3:6e6f:794a with SMTP id 6a1803df08f44-6cb1dd4325dmr95335336d6.20.1727360557978; Thu, 26 Sep 2024 07:22:37 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?Q?Rasmus_M=C3=B8gelberg?= Date: Thu, 26 Sep 2024 16:22:27 +0200 Message-ID: Subject: [HoTT] Types post-proceedings call for papers To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000751f1f0623067888" X-Original-Sender: rmogelberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=lzAykFHu; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::732 as permitted sender) smtp.mailfrom=rmogelberg@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: , --000000000000751f1f0623067888 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2024 was held from 10 to 14 June at the IT University of Copenhagen, Denmark. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings. Submission Guidelines Submission is open to everyone, also to those who did not participate in the TYPES 2024 conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, and be original, i.e. neither previously published, nor simultaneously submitted to a journal or a conference. - Papers have to be formatted with the current LIPIcs style and adhere to the style requirements of LIPIcs. - The upper limit for the length of submissions is 20 pages for the main text (including appendices, but excluding title-page and bibliography). - Papers must be submitted as PDF via the EasyChair interface, accessible at https://easychair.org/conferences/?conf=3Dposttypes24 - Authors have the option to attach to their submission a zip or tgz file containing code (formalised proofs or programs), but reviewers are not obliged to take the attachments into account and they will not be published. Deadlines - Abstract Submission : 31 October 2024 (AoE) - Paper submission: 2 December 2024 (AoE) - Author notification: 31 March 2025 List of Topics The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics: - Foundations of type theory; - Applications of type theory (e.g. linguistics or concurrency); - Constructive mathematics; - Dependently typed programming; - Industrial uses of type theory technology; - Meta-theoretic studies of type systems; - Proof assistants and proof technology; - Automation in computer-assisted reasoning; - Links between type theory and functional programming; - Formalising mathematics using type theory; - Homotopy type theory and univalent mathematics. Editors Rasmus Ejlers M=C3=B8gelberg, IT University of Copenhagen, Denmark Benno van den Berg, Universiteit van Amsterdam, The Netherlands Contact In case of questions, contact EMAIL posttypes24@easychair.org --=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/CAO0VQQavcGg4DVeXCwxX8tg2_08SmmJbRMH1PPnej0BZdO%3DsEw%40= mail.gmail.com. --000000000000751f1f0623067888 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
TYPES is a major forum for the presentation of research on= all aspects
of type theory and its applications. TYPES 2024 was held fr= om 10 to 14
June at the IT University of Copenhagen, Denmark. The
pos= t-proceedings volume will be published in LIPIcs, Leibniz
International = Proceedings in Informatics, an open-access series of
conference proceedi= ngs.

Submission Guidelines

Submission is open to everyone, al= so to those who did not participate
in the TYPES 2024 conference. We wel= come high-quality descriptions of
original work, as well as position pap= ers, overview papers, and system
descriptions. Submissions should be wri= tten in English, and be original,
i.e. neither previously published, nor= simultaneously submitted to a
journal or a conference.

- Papers= have to be formatted with the current LIPIcs style and adhere
=C2=A0 to= the style requirements of LIPIcs.

- The upper limit for the length = of submissions is 20 pages for the
=C2=A0 main text (including appendice= s, but excluding title-page and
=C2=A0 bibliography).

- Papers mu= st be submitted as PDF via the EasyChair interface,
=C2=A0 accessible at= https://= easychair.org/conferences/?conf=3Dposttypes24

- Authors have the= option to attach to their submission a zip or tgz
=C2=A0 file containin= g code (formalised proofs or programs), but reviewers
=C2=A0 are not obl= iged to take the attachments into account and they will
=C2=A0 not be pu= blished.

Deadlines

- Abstract Submission : 31 October 2024 (A= oE)
- Paper submission: 2 December 2024 (AoE)
- Author notification= : 31 March 2025

List of Topics

The scope of the post-proceedi= ngs is the same as the scope of the
conference: the theory and practice = of type theory. In particular, we
welcome submissions on the following t= opics:

- Foundations of type theory;
- Applications of type theor= y (e.g. linguistics or concurrency);
- Constructive mathematics;
- De= pendently typed programming;
- Industrial uses of type theory technology= ;
- Meta-theoretic studies of type systems;
- Proof assistants and pr= oof technology;
- Automation in computer-assisted reasoning;
- Links = between type theory and functional programming;
- Formalising mathematic= s using type theory;
- Homotopy type theory and univalent mathematics.
Editors

Rasmus Ejlers M=C3=B8gelberg, IT University of Copenha= gen, Denmark
Benno van den Berg, Universiteit van Amsterdam, The Netherl= ands

Contact

In case of questions, contact EMAIL posttypes24@easychair.org

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAO0VQQavcGg4DVeXCwxX8tg2_08Smm= JbRMH1PPnej0BZdO%3DsEw%40mail.gmail.com.
--000000000000751f1f0623067888--