From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10868 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Steve Zdancewic Newsgroups: gmane.comp.lang.ats.questions,gmane.science.mathematics.logic.acl2.general,gmane.comp.lang.agda,gmane.comp.lang.caml.inria,gmane.science.mathematics.categories,gmane.science.mathematics.logic.isabelle.user,gmane.science.mathematics.logic.coq.club,gmane.comp.lang.haskell.general,gmane.comp.mathematics.hol,gmane.comp.lang.idris.general,gmane.science.mathematics.logic.lean.user,gmane.science.mathematics.prooftheory,gmane.science.mathematics.logic.coq.ssreflect Subject: Certified Programs and Proofs (CPP) 2023: Call for Participation Date: Mon, 5 Dec 2022 17:00:28 -0500 Message-ID: Reply-To: ats-lang-users-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="23185"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:102.0) Gecko/20100101 Thunderbird/102.5.1 To: acl2-wNjIbZq71S3S/e0kzai8jze48wsgrGvP@public.gmane.org, agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, appsem-YE1jQ5a0g27r6u3/gjwTbCOeiWZ7kpuZ@public.gmane.org, ats-lang-users-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org, caml-list-MZpvjPyXg2s@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, cl-isabelle-users-33AaDErTWvBK/gkPnarB6Q@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org, dl-N/hjgmPSN2rYtjvyW6yDsg@public.gmane.org, event-HKdKWCMRuSoyzp8zgePYoYQuADTiUCJX@public.gmane.org, finite-model-theory-JyGdfDITRCtaq5fyzuukUWfrygkm6VTR@public.gmane.org, fm-announcements-cwGa0Mn2PPIb0b0yYlRVAg@public.gmane.org, folli-WRVizKnH2qah6J55Ss3d3w@public.gmane.org, fom-+I05ep9qJbk3uPMLIKxrzw@public.gmane.org, fstar-club-bM+ny+RY8h+a+bCvCPl5/gCzwTLBPCX0@public.gmane.org, GAMES-JyGdfDITRCtaq5fyzuukUWfrygkm6VTR@public.gmane.org, grin-eventi-q19zApnVckaMVPazPUTyfzUZDU+1vuVT@public.gmane.org, haskell-HC+Z4NTRIlBAfugRpC6u6w@public.gmane.org, hol-info-5NWGOfrQmneRv+LV9MX5uipxlwaOVQ5f@public.gmane.org, ic.eatcs.di-AvPnZcJwPP15YBQjdAIqgE6FHaWFtxp8@public.gmane.org, idris-lang-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org, las-lics-Xt5XgHjqiBV35pIdRWVIsoQuADTiUCJX@public.gmane.org, lean-user-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org, logic-o02PS0xoJP/q4qjOmvqfQQ@public.gmane.org, loginf-YE1jQ5a0g27r6u3/gjwTbCOeiWZ7kpuZ@public.gmane.org, matryoshka-devel-bM+ny+RY8h+a+bCvCPl5/gCzwTLBPCX0@public.gmane.org, PlanetKR-7hZN9r6sC8U@public.gmane.org, ProofTheory-0VDFhBbLC1Y8tAQEoGlWAQ@public.gmane.org, pvs-1VPwtPCARB1BDgjK7y7TUQ@public.gmane.org, rewriting-vYW+cPY1g1pWj0EZb7rXcA@public.gmane.org, rewriting-URqwlNng3RYeRlMTHcmXLbhJywXYPV/v@public.gmane.org, srepls-BJlGqfXgjbjQzY9nttDBhA@public.gmane.org, ssreflect-C19eNOrLonWacSAJ64KLvA@public.gmane.org Original-X-From: ats-lang-users+bncBDR4XNXSWQLRB76TXGOAMGQEQXGVFQY-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org Mon Dec 05 23:00:32 2022 Return-path: Envelope-to: gclaq-ats-lang-users@m.gmane-mx.org Original-Received: from mail-il1-f188.google.com ([209.85.166.188]) by ciao.gmane.io with esmtps (TLS1.3:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.92) (envelope-from ) id 1p2JVo-0005oH-Jh for gclaq-ats-lang-users@m.gmane-mx.org; Mon, 05 Dec 2022 23:00:32 +0100 Original-Received: by mail-il1-f188.google.com with SMTP id a13-20020a056e0208ad00b003034c36b8b5sf6161402ilt.9 for ; Mon, 05 Dec 2022 14:00:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1670277631; cv=pass; d=google.com; s=arc-20160816; b=w67TWr+hYkwsweYBexzyOJGQjgH3rzS8e615cj1Jrza8NEj/wx7lXkKV6FoJKYigRW J1Pm0USffVg2UkioKC0ozhpF+3g/n1zce3+dzoNTnPuT7W69/PiV2uTuq3rYZYMtUi9Q 0v3k+jZ+u/E7Crt65U6QhSjn/1US8vgYqWoHiS3MpecCIAIwVE/ibnBxBSDmqqsN7tHc rirsQmnln7wyeHRUNepbM/2hVskcyiOtokiMjHk9au57G4KPicmGeJafCfKD/e0/46H+ PTpjhhFm66PPFOImRoNsLs/pjP+KryDr/n7efB8qq2T4WHQjHiapkWS5c09cAtQzTJGQ hLLQ== 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:reply-to:content-transfer-encoding :to:subject:from:content-language:user-agent:mime-version:date :message-id:sender:dkim-signature; bh=vNYC9U1S2LsCj8a7H18xO0EI3e41CRyJVx/0uierQtY=; b=HHXqZlFvboxzx4OVh/6uHx4sx/FgKOygR6SWVlVN2P/2jtIScVb/Ekejex8JFQfWrS HxJbzR7kmT0LYn34Cu0/qPeOOTChNG2m4VCVl+a43DIvG4nUZRCVgDz6rZMnDFZMePrf a599cLT4zd2piLO+UELvOT9lzV5FROqAHm05hokpErxCgadyXGGIzlTeop4KvXtLw1iY Kt6lQJB64MI41K8AOpPEl+5tMPNYxbHgfAWIvdQ9kThU7XIQylYWavCwAmrWIxWswXov xcEXQHb0XiUhspLAVlmyGEGJ2uaxi1C4h5PVg/PBfVeky7YsmPhzIZryDyoif2nfGe7t IAhQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@seas-upenn-edu.20210112.gappssmtp.com header.s=20210112 header.b=ZYVmElU0; spf=pass (google.com: domain of stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=upenn.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender :content-transfer-encoding:to:subject:from:content-language :user-agent:mime-version:date:message-id:sender:from:to:cc:subject :date:message-id:reply-to; bh=vNYC9U1S2LsCj8a7H18xO0EI3e41CRyJVx/0uierQtY=; b=GCXfp3/YTrMjpV1kzm9SaeacqNJwIvb6zDrVX5iipchDyM1QtMx3gbzyfxYygcVL+V P818HdW4gQgIvqRcisF+yA1eLo7aBRrfuQbXO1xg66yJOr34gHG8P94JbuVP0ZK8gS69 mY23Fd8/hezswIzBOj1bns6NYsBI48owqehZwxQUhFM9Ff3uTTYtPrkDgwCn8WofAYu1 xVJSzlv3yGNkTC/6kjzGS/B7W6pvboKvdyijtI1ia2K8cBuyUhStW4+G23BvY1VD12MG njZo4xVxA5/5UXzo/sNiB0Ae8mdDutCipxChu/p/TtaemyI1pK6nWtu/sHtv X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender :content-transfer-encoding:to:subject:from:content-language :user-agent:mime-version:date:message-id:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=vNYC9U1S2LsCj8a7H18xO0EI3e41CRyJVx/0uierQtY=; b=znUgdxElBqMJTWxZ6+3ME1NY2knD3AadbTCzR1z7ROtf++W5LdoeTQIfNCkNoy952S GaLboFYpiR0gdyScIJ9uH8MPQPkrWlbgMPPPfeUkn8tvh5rNoZEsS9dyqMFRATVbPjUP Ivy9E5fiiAE5ifVgGkJ9RpUxUdI6Fy2W/ImS1YdPUqg4HbWNC41e2EBWjfOg1XFiANi3 sdVys9mSMbYHSya8sB3vkBheCazGB7wRlUT8ie7XFWiFnezpOSQcDX99G0Ep1Ev5a9gV ehYonPfOvuKTxdD Original-Sender: ats-lang-users-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org X-Gm-Message-State: ANoB5plRQakvz99Lc//Lar17aEVTHIk18FJN4Elmj+s1I+NZmVKT8tyG yCH8JKCjjuM1l6IHgbIaHnw= X-Google-Smtp-Source: AA0mqf7WYF8VbM+ObDc+OxFfTjmBZDiGjJ0oASRvsr9uUdLgf2s5wSt5bOcoXiCfaLKrJyBpVx4leA== X-Received: by 2002:a05:6e02:102f:b0:300:f452:339b with SMTP id o15-20020a056e02102f00b00300f452339bmr29850362ilj.306.1670277631420; Mon, 05 Dec 2022 14:00:31 -0800 (PST) X-BeenThere: ats-lang-users-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org Original-Received: by 2002:a02:9524:0:b0:375:19d7:7919 with SMTP id y33-20020a029524000000b0037519d77919ls904614jah.8.-pod-prod-gmail; Mon, 05 Dec 2022 14:00:30 -0800 (PST) X-Received: by 2002:a02:711c:0:b0:375:aa4:a8f with SMTP id n28-20020a02711c000000b003750aa40a8fmr38871834jac.247.1670277630754; Mon, 05 Dec 2022 14:00:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1670277630; cv=none; d=google.com; s=arc-20160816; b=QNdLrnFw00KxV5mRcMjxda9tn7bYRYwvPSGQcSeORz6eoSqQg72dz1YM2b5/p1ULTA SrMgOiLtuhOn40uDymNbAunXO+RcDUVw6rpRKmeEvE1OZaT6ZrrjZgVByrj6c7POD/wG GqLWnJKXlsubDpcRjcem8nUg7klwBRZNg9psGay9VDn0eok+QXhPDFwzNJVcpOIdOiZM K32MjElFYHwdxXW1ROlht6IDWWLEXEAjilfBSyy8s/NcLLpIqIDHicu8xxzcbSdCLIW5 j9SGmwLMLJwXMRiNsZG1dtL09bChxyu1umqtH990v5cKtuwvQkMwmXevRCN9g+fhjLtT Qaww== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:from:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=EvW0OpGYM8KE3u3vRH85RvBiU11SKck8Z8YIXgQ+3nQ=; b=SkySWRc4mT6ry7y9evoqlAc0YcbPmXgPLYrfXqMAfzSuWKG7F30WG3dHBM9KF23Tqo zZAWGZeBTsWu0aLjAl/FmqsTaVk5dGvFSi+SqfnFyoQpFkN11E+KKB1ogijPVs/IV6Pb svQ4x1CMVvTq/maVZP5fmriNm+O5CVRiuSyUffC+5SH0tN7ThBW6wNFsYoOUJjmAFBeF ohd5LV1WKCxsnvAjNgEnMWBgtsMhyC+Grnv7flZ1SFSVoYvptRPKNm8JsptLS5/XeTUU gLwo7NL2F5eAL01qylCVO8deqEL/dum8b1p2JZ8ikSjdtXscfvTbu3d70kjkVQA6bSy1 3NMg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@seas-upenn-edu.20210112.gappssmtp.com header.s=20210112 header.b=ZYVmElU0; spf=pass (google.com: domain of stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=upenn.edu Original-Received: from mail-qt1-x82a.google.com (mail-qt1-x82a.google.com. [2607:f8b0:4864:20::82a]) by gmr-mx.google.com with ESMTPS id v11-20020a02b90b000000b0038a5b827993si31037jan.2.2022.12.05.14.00.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 05 Dec 2022 14:00:30 -0800 (PST) Received-SPF: pass (google.com: domain of stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org designates 2607:f8b0:4864:20::82a as permitted sender) client-ip=2607:f8b0:4864:20::82a; Original-Received: by mail-qt1-x82a.google.com with SMTP id fz10so12492755qtb.3 for ; Mon, 05 Dec 2022 14:00:30 -0800 (PST) X-Received: by 2002:a05:622a:1a94:b0:3a7:e4cb:3ff6 with SMTP id s20-20020a05622a1a9400b003a7e4cb3ff6mr5181834qtc.570.1670277630168; Mon, 05 Dec 2022 14:00:30 -0800 (PST) Original-Received: from ?IPV6:2607:f470:6:1001:4128:664e:6f99:2431? ([2607:f470:6:1001:4128:664e:6f99:2431]) by smtp.gmail.com with ESMTPSA id f25-20020ac86ed9000000b003a4f2510e5dsm10314710qtv.24.2022.12.05.14.00.28 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 05 Dec 2022 14:00:29 -0800 (PST) Content-Language: en-US X-Original-Sender: stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@seas-upenn-edu.20210112.gappssmtp.com header.s=20210112 header.b=ZYVmElU0; spf=pass (google.com: domain of stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=stevez-hkHJxBBPWjbG6jMu9gPlYQ@public.gmane.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=upenn.edu Precedence: list Mailing-list: list ats-lang-users-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org; contact ats-lang-users+owners-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org List-ID: X-Google-Group-Id: 946475932186 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , Xref: news.gmane.io gmane.comp.lang.ats.questions:6549 gmane.science.mathematics.logic.acl2.general:1261 gmane.comp.lang.agda:13066 gmane.comp.lang.caml.inria:69892 gmane.science.mathematics.categories:10868 gmane.science.mathematics.logic.isabelle.user:17999 gmane.science.mathematics.logic.coq.club:23174 gmane.comp.lang.haskell.general:22741 gmane.comp.mathematics.hol:6487 gmane.comp.lang.idris.general:6653 gmane.science.mathematics.logic.lean.user:1461 gmane.science.mathematics.prooftheory:1691 gmane.science.mathematics.logic.coq.ssreflect:55 Archived-At: *** Call for Participation *** *** Certified Programs and Proofs (CPP) 2023 *** =C2=A0- Early registration deadline: 16 December 2022 =C2=A0- Registration: https://popl23.sigplan.org/attending/registration =C2=A0- Further reduced student participation fee: see below =C2=A0- Accommodation: Boston Park Plaza =C2=A0=C2=A0 https://popl23.sigplan.org/venue/POPL-2023-venue Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education. CPP 2023 (https://popl23.sigplan.org/home/CPP-2023) will be held on 16-17 January 2023 and will be co-located with POPL 2023. CPP 2023 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG, and supported by a diverse set of industrial sponsors. Similarly to other events collocated with POPL 2023, CPP will take place as an in-person event at Boston Park Plaza, and will require attendees to provide proof of vaccination (details will be available soon). Virtual participation via Airmeet will also be available; look for updated information about that option on the POPL web site. For more information about this edition and the CPP series, please visit https://popl23.sigplan.org/home/CPP-2023 ### Invited Speakers * Sandrine Blazy, University of Rennes and IRISA * Cezary Kaliszyk, University of Innsbruck ### Accepted papers The list of accepted papers is available at https://popl23.sigplan.org/home/CPP-2023#event-overview ### Subsidized student registration To facilitate in-person participation, CPP 2023 offers the opportunity=20 to waive the registration fees for those that are in need of financial support to=20 attend the conference. This support is particularly aimed at undergraduate and=20 graduate students, postdocs, and those from marginalized groups. If you wish to apply for support you may do so by sending an email to=20 the CPP conference co-chairs (Dmitriy Traytel and Robbert Krebbers, see below=20 for their email addresses), with a brief description of your situation. The=20 deadline for applications is 11 December 2022, 23:59 AoE. Notifications will be sent=20 out at most two days later; hence, those who cannot be supported will still=20 have the opportunity to register with the regular early registration fee before 16 December. Applications arriving after 11 December will be considered only i= f additional budget is remaining. CPP's student support is made possible by our generous industrial=20 supporters: https://popl23.sigplan.org/home/CPP-2023#About ### Contact For any questions please contact the chairs: Steve Zdancewic (PC co-chair) Brigitte Pientka (PC co-chair) Robbert Krebbers (conference co-chair) Dmitriy Traytel (conference co-chair) --=20 You received this message because you are subscribed to the Google Groups "= ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to ats-lang-users+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/Ez6ZCGd0@public.gmane.org To view this discussion on the web visit https://groups.google.com/d/msgid/= ats-lang-users/f8bcc439-135e-291f-6974-1e8f34ceaa81%40seas.upenn.edu.