From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 14588 invoked from network); 14 Jul 2023 17:21:27 -0000 Received: from mail-wr1-x437.google.com (2a00:1450:4864:20::437) by inbox.vuxu.org with ESMTPUTF8; 14 Jul 2023 17:21:27 -0000 Received: by mail-wr1-x437.google.com with SMTP id ffacd0b85a97d-313c930ee0esf1254434f8f.0 for ; Fri, 14 Jul 2023 10:21:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1689355286; cv=pass; d=google.com; s=arc-20160816; b=unG8RwFDHmr4Kc9tTU6Ooyl0xfzBFP/XNYnhHgs5VMLXhWMWSjjlZPi+E9lTQuGvNY rYTdOsEMtmyZPZNwa2gBWQbJ4xNA6PADFIvHaOtkvLdrxaO3ellArL6tZEGbSwoqdh2R tgYzv7iJlAudYl2yS2yjCl5AhuaWI7efZSY+SDM9VoPLB9lVmnKAf2FkRKrNR2Ty4nOg m8rdfdpY50uYuH3Doi5osDuwPE8LEvNgFKf0IDP2WjGC/iTtzVPjNqy9L9V85tT2Emjx 17OfNfqy742ClYhyIgjvZQzcbbYfp5vN0tRxw5ZcjA7HYZlqizmKJImh+MsjDKHku0Rc 2TXw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-transfer-encoding :content-language:to:subject:from:user-agent:mime-version:date :message-id:sender:dkim-signature:dkim-signature; bh=2Qv6z0cdrHNVVtuVY6pVBkm/gF4D9+LEXgR6omZ9zZ0=; fh=51nBikT8l9U/IMDIE0qFjr4eI9v3q05WnVRzJXeTsmo=; b=HCx02WdzL1fk0iv66e0taixHE3QJEuS6ndN7JQ0IPj05EDpB/TOCJZWbbskzl+Ppxt FcrSyfXYA9vjrgoenjOkv2PjC+ScEKP4xK4tWDkCiYK6iMG3Mp26z1TfbVcehOti5VE7 tUyuO57si/kvOdP/Z85ufxyQG/kBGeEBEvlvzVRXWk7j8QPUXzZX+6XG6005l/Qlv17U eUVxnyQiia/FLGZzBR/aYnAqExZR5rKvsK7sv8Hj9hROjWHHgtt6QyFynhsXRKziuzOM XHYLqQM0FR2CakuUPpjiw7qgVFtGewjO6jIpbp110FYDRyO3ehEsdSA303gtDDZdbo6F DtJQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=b5DC7jat; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52c as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1689355286; x=1691947286; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:content-language:to :subject:from:user-agent:mime-version:date:message-id:sender:from:to :cc:subject:date:message-id:reply-to; bh=2Qv6z0cdrHNVVtuVY6pVBkm/gF4D9+LEXgR6omZ9zZ0=; b=mgcZeEN/xuyEICxPRYzw3UUx6ilo+KbQnrYFwkBbC93oEa4MvJYtpvHk7Seum8Z2ZK leUwXJaFYa2kmpyGrCNxJG6WS7wwGzryLEBFnp7BdOZaqfWWDqCNj5DPRCTsYoKMK4lD wUl+0QyhhDxdvUWNP+vXAgvhdPJRFO/jnXz4BKk0E86jVD5ea6U4ReSyhQ/m2i6Ppngz kjg45Prqb5LVAu8TgL21TM8PNiY98xQAHiryJ/zYQyK5gJiTYZAFGrSZgUqydFEqmWGU ra2RX+Xt+YCqpjo3SOjj5+QbY2day1LFDElvzs4SiKOslwBQ1KIpjOX/gq0u2jttzYBD iKag== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1689355286; x=1691947286; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:content-language:to :subject:from:user-agent:mime-version:date:message-id:from:to:cc :subject:date:message-id:reply-to; bh=2Qv6z0cdrHNVVtuVY6pVBkm/gF4D9+LEXgR6omZ9zZ0=; b=j7ON+JfzMFnXma5w2qt8BUNHzCfErZrTUeoQ6UA7w9Hj761W+jDbIwiAXOcNu4/jw7 ys3AV07VBoh2dRxRKCTTYt52tzDgz0RVz1svM8gA+RlWSi6HaUtT5K/4QYK8/T9BhcTV qnhAXhyk3yZjf+5L+82oPx1onTKm0y1dr0kcEkL7pOXkttSbp2XL3hhyam5GJpVbUnXS nnPkrqX3BCdH6iZoGS/4a61Vd9gkzYUNkw6/lpSrxorsLpVTDt70eIhR9ejnl01uC5I0 utRVzILKZ04I4CoWnle5CtbOXdEAqKn2AFRWbTAjE9CQnlAkECpsjtgYG4XHDi8yDutf +dTg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1689355286; x=1691947286; 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 :content-transfer-encoding:content-language:to:subject:from :user-agent:mime-version:date:message-id:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=2Qv6z0cdrHNVVtuVY6pVBkm/gF4D9+LEXgR6omZ9zZ0=; b=CrZM3Sv+/p/6fsLRfv9QJJ33MSltq0lqzAnaxJqYg8/JnTu16v7PosT2JwPyENiA3Q rYVE25das8OhmkmwxUxoISTVhozED3D15uVP/K76B/pomkvdq5x4vtlkRvU0/zDEiTxO N2HSVvA/r7dzVqW4/ICTVmpxYP4fpIxEYzEWez6v/H4vpiKe5WfjqqQUFgpGO/0okAQ+ vcrUw+aHw/XU8hloSllpEblh+isuLLitvlHb3pc0xynRYM1PazR6qjeZ8poHrju8gLL1 sTp0MMkSMWjg6BYLC5yhMb4hekKxvsxvCxUaKBMF9FTJiO6/T9ynHAzKbWxMM5qlJwZY GhMA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLbxVGFi3Kv9chJHu147ze2yffmVA8VFUv4ma+hOWWDRuEI/u9Nf kAoRLIEUhN3pyR2AtIfrnF4= X-Google-Smtp-Source: APBJJlG5+lyTBHbZ1IoD9ZQ+83+PM05v+s+1D8OsDbcvy4//EO9V1NaAgkhB0Yc5a91YKtqWD6o5ww== X-Received: by 2002:adf:fe4b:0:b0:316:f24b:597a with SMTP id m11-20020adffe4b000000b00316f24b597amr783987wrs.46.1689355285990; Fri, 14 Jul 2023 10:21:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:f28c:0:b0:312:831e:b4c2 with SMTP id k12-20020adff28c000000b00312831eb4c2ls700498wro.2.-pod-prod-03-eu; Fri, 14 Jul 2023 10:21:23 -0700 (PDT) X-Received: by 2002:a7b:c383:0:b0:3fc:9e:eead with SMTP id s3-20020a7bc383000000b003fc009eeeadmr4446815wmj.20.1689355283009; Fri, 14 Jul 2023 10:21:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1689355282; cv=none; d=google.com; s=arc-20160816; b=V1Ck9G8vvTjIaEEcmENPaxpt78mZ2htBbZAe0d2xOlxQttJ1eaxXp1RBVeiAh4cQRi zJwZOMIx5gtWkLo8O3V+MtdmjsKdWC5+5d4FkmO67Vy6omP3GHDItB4rwPWNpAYd1Rif QEekedmTaylATPBSQlxkFrDgsyJFYBC+NeAkzdR6LGFqzZ71czvlnPVUWX2NfHZVbRb6 MBUenlNihYF9+kn8iT/0ULuoLJSgRlj2Umrro05JojiIp1Vai2018yH0x1Ca3gfGnHzb Ha7IIaVUIWSNkn2vyZWUDxusUHzNZF9r3ux0Q2dTLozFdjoqSwgFnbZEktFSgqqi+ONE Ot9g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:to:subject:from :user-agent:mime-version:date:message-id:dkim-signature; bh=OggkHw9XENKMyz9NCBnwLjuvmmf1uFI/nY6XHMwBQmw=; fh=51nBikT8l9U/IMDIE0qFjr4eI9v3q05WnVRzJXeTsmo=; b=ibPb3xesZM0OfMqG/1D+UBJ2NrihaqF+0e6N1xCtXzXXHMJkvSW96YjL3gmbLfWDW1 g2RnJblb/gW1Ts1kkeuEZfjxFYtO8TcKhVsLyfyjx4/S24SEFe1bbpG8XkKMoASTW4Uw MoydYC/kpLWhyTANdwOBhU3cGV5JH4+ggepRxYlMMFpdWWAGIM1DJBtm4ytVE0l9dZI4 wJOTb7PW1ieGjJELFAWKytDtjBasEBfx82kTLVIrFZSSwDr0oWgsYycFdaXmaWsL75tF Ydy1IxEm64uAJOfFkeWDG6TbbRY9B55sAMd5eseXt2E172h6yXJP4PDAFdmQBqesv8uW gxtg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=b5DC7jat; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52c as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52c.google.com (mail-ed1-x52c.google.com. [2a00:1450:4864:20::52c]) by gmr-mx.google.com with ESMTPS id fk8-20020a05600c0cc800b003fbca831b48si114264wmb.2.2023.07.14.10.21.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 14 Jul 2023 10:21:22 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52c as permitted sender) client-ip=2a00:1450:4864:20::52c; Received: by mail-ed1-x52c.google.com with SMTP id 4fb4d7f45d1cf-5216569f9e3so875109a12.0 for ; Fri, 14 Jul 2023 10:21:22 -0700 (PDT) X-Received: by 2002:a17:907:d0d:b0:988:9b29:5653 with SMTP id gn13-20020a1709070d0d00b009889b295653mr4938223ejc.77.1689355282369; Fri, 14 Jul 2023 10:21:22 -0700 (PDT) Received: from ?IPV6:2001:1c00:b92:b700:ef60:93e4:fdd5:4d81? (2001-1c00-0b92-b700-ef60-93e4-fdd5-4d81.cable.dynamic.v6.ziggo.nl. [2001:1c00:b92:b700:ef60:93e4:fdd5:4d81]) by smtp.gmail.com with ESMTPSA id g14-20020a17090613ce00b00992665694f7sm5654726ejc.107.2023.07.14.10.21.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 14 Jul 2023 10:21:22 -0700 (PDT) Message-ID: <8cad9de9-898a-49e4-67b3-2489233208cc@gmail.com> Date: Fri, 14 Jul 2023 19:21:21 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.13.0 From: Benedikt Ahrens Subject: [HoTT] 1st CFP - CPP 2024 - Certified Programs and Proofs To: homotopytypetheory@googlegroups.com Content-Language: en-US Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=b5DC7jat; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52c as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , Certified Programs and Proofs (CPP) is an international conference on=20 practical and theoretical topics in all areas that consider formal=20 verification and certification as an essential paradigm for their work.=20 CPP spans areas of computer science, mathematics, logic, and education. CPP 2024 (https://popl24.sigplan.org/home/CPP-2024) will be held on=20 15-16 January 2024 and will be co-located with POPL 2024 in London, UK.=20 CPP 2024 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2024 will welcome contributions from all members of the community.=20 The CPP 2024 organizers will strive to enable both in-person and remote=20 participation, in cooperation with the POPL 2024 organizers. IMPORTANT DATES * Abstract Submission Deadline: 12 September 2023 at 23:59 AoE (UTC-12h) * Paper Submission Deadline: 19 September 2023 at 23:59 AoE (UTC-12h) * Notification (tentative): 21 November 2023 * Camera Ready Deadline (tentative): Mid December 2023 (TBA) * Conference: 15-16 January 2024 Deadlines expire at the end of the day, anywhere on earth. Abstract and=20 submission deadlines are strict and there will be no extensions. DISTINGUISHED PAPER AWARDS Around 10% of the accepted papers at CPP 2024 will be designated as=20 Distinguished Papers. This award highlights papers that the CPP program=20 committee thinks should be read by a broad audience due to their=20 relevance, originality, significance and clarity. TOPICS OF INTEREST We welcome submissions in research areas related to formal certification=20 of programs and proofs. The following is a non-exhaustive list of topics=20 of interest to CPP: * certified or certifying programming, compilation, linking, OS kernels,=20 runtime systems, security monitors, and hardware; * certified mathematical libraries and mathematical theorems; * proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light,=20 Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc); * new languages and tools for certified programming; * program analysis, program verification, and program synthesis; * program logics, type systems, and semantics for certified code; * logics for certifying concurrent and distributed systems; * mechanized metatheory, formalized programming language semantics, and=20 logical frameworks; * higher-order logics, dependent type theory, proof theory, logical=20 systems, separation logics, and logics for security; * verification of correctness and security properties; * formally verified blockchains and smart contracts; * certificates for decision procedures, including linear algebra,=20 polynomial systems, SAT, SMT, and unification in algebras of interest; * certificates for semi-decision procedures, including equality,=20 first-order logic, and higher-order unification; * certificates for program termination; * formal models of computation; * mechanized (un)decidability and computational complexity proofs; * formally certified methods for induction and coinduction; * integration of interactive and automated provers; * logical foundations of proof assistants; * applications of AI and machine learning to formal certification; * user interfaces for proof assistants and theorem provers; * teaching mathematics and computer science with proof assistants. SUBMISSION GUIDELINES Prior to the paper submission deadline, the authors should upload their=20 anonymized paper in PDF format through the HotCRP system at https://cpp2024.hotcrp.com The submissions must be written in English and provide sufficient detail=20 to allow the program committee to assess the merits of the contribution.=20 They must be formatted following the ACM SIGPLAN Proceedings format=20 using the acmart style with the sigplan option, which provides a=20 two-column style, using 10 point font for the main text, and a header=20 for double blind review submission, i.e., \documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfol= ios=3Dtrue,printccs=3Dfalse,printacmref=3Dfalse} The submitted papers should not exceed 12 pages, including tables and=20 figures, but excluding bibliography and clearly marked appendices. The=20 papers should be self-contained without the appendices. Shorter papers=20 are welcome and will be given equal consideration. Submissions not=20 conforming to the requirements concerning format and maximum length may=20 be rejected without further consideration. CPP 2024 will employ a lightweight double-blind reviewing process=20 following the process from previous years. To facilitate this, the=20 submissions must adhere to two rules: (1) author names and institutions must be omitted, and (2) references to authors=E2=80=99 own related work should be in the third= =20 person (e.g., not "We build on our previous work ..." but rather "We=20 build on the work of ..."). The purpose of this process is to help the PC and external reviewers=20 come to an initial judgment about the paper without bias, not to make it=20 impossible for them to discover the authors if they were to try. Nothing=20 should be done in the name of anonymity that weakens the submission or=20 makes the job of reviewing it more difficult. In particular, important=20 background references should not be omitted or anonymized. In addition,=20 authors are free to disseminate their ideas or draft versions of their=20 papers as usual. For example, authors may post drafts of their papers on=20 the web or give talks on their research ideas. Note that POPL 2024=20 itself will employ full double-blind reviewing, which differs from the=20 light-weight CPP process. This FAQ from previous SIGPLAN conference=20 addresses many common concerns:=20 https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-R= eviewing-FAQ We strongly encourage the authors to provide any supplementary material=20 that supports the claims made in the paper, such as proof scripts or=20 experimental data. This material must be uploaded at submission time, as=20 an archive, not via a URL. Two forms of supplementary material may be=20 submitted: (1) Anonymous supplementary material is made available to the reviewers=20 before they submit their first-draft reviews. (2) Non-anonymous supplementary material is made available to the=20 reviewers after they have submitted their first-draft reviews and have=20 learned the identity of the authors. Please use anonymous supplementary material whenever possible, so that=20 it can be taken into account from the beginning of the reviewing process. The submitted papers must adhere to the SIGPLAN Republication Policy=20 (https://www.sigplan.org/Resources/Policies/Republication/) and the ACM=20 Policy on Plagiarism=20 (https://www.acm.org/publications/policies/plagiarism). Concurrent=20 submissions to other conferences, journals, workshops with proceedings,=20 or similar forums of publication are not allowed. The PC chairs should=20 be informed of closely related work submitted to a conference or journal=20 in advance of submission. One author of each accepted paper is expected=20 to present it at the (possibly virtual) conference. PUBLICATION, COPYRIGHT AND OPEN ACCESS The CPP 2024 proceedings will be published by the ACM, and authors of=20 accepted papers will be required to choose one of the following=20 publication options: (1) Author retains copyright of the work and grants ACM a non-exclusive=20 permission-to-publish license and, optionally, licenses the work under a=20 Creative Commons license. (2) Author retains copyright of the work and grants ACM an exclusive=20 permission-to-publish license. (3) Author transfers copyright of the work to ACM. For authors who can afford it, we recommend option (1), which will make=20 the paper Gold Open Access, and also encourage such authors to license=20 their work under the CC-BY license. ACM will charge you an article=20 processing fee for this option (currently, US$700), which you have to=20 pay directly with the ACM. You don=E2=80=99t need to pay this fee if the=20 corresponding author=E2=80=99s affiliating institution is part of ACM OPEN= =20 (https://libraries.acm.org/subscriptions-access/open-participants). For everyone else, we recommend option (2), which is free and allows you=20 to achieve Green Open Access, by uploading a preprint of your paper to a=20 repository that guarantees permanent archival such as arXiv or HAL. This=20 is anyway a good idea for timely dissemination even if you chose option 1. The official CPP 2024 proceedings will also be available via SIGPLAN=20 OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM=E2=80=99s take on this, see their Copyright Policy=20 (http://www.acm.org/publications/policies/copyright-policy) and Author=20 Rights (http://authors.acm.org/main.html). Sandrine Blazy, University of Rennes, France (co-chair) Brigitte Pientka, McGill University, Canada (co-chair) ORGANIZERS Amin Timany, Aarhus University, Denmark (conference co-chair) Dmitriy Traytel, University of Copenhagen, Denmark (conference co-chair) Sandrine Blazy, University of Rennes (PC co-chair) Brigitte Pientka, McGill University, Canada (PC co-chair) CONTACT For any questions please contact the two PC chairs: Sandrine Blazy Brigitte Pientka --=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/8cad9de9-898a-49e4-67b3-2489233208cc%40gmail.com.