From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 166AF5D5 for ; Thu, 9 Dec 2021 13:35:31 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.88,192,1635199200"; d="scan'208,217";a="9736566" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 09 Dec 2021 14:35:30 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 5B86AE016E; Thu, 9 Dec 2021 14:35:29 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id DE282E0244 for ; Thu, 9 Dec 2021 14:35:25 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stevez@seas.upenn.edu; spf=Pass smtp.mailfrom=stevez@seas.upenn.edu; spf=None smtp.helo=postmaster@mail-qv1-f42.google.com IronPort-PHdr: =?us-ascii?q?A9a23=3AG+8VcRCokpsWRnKaFY9lUyQUU0QY04WdBeb1wqQ?= =?us-ascii?q?uh78GSKm/5ZOqZBWZua80yg+RFtiCo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/t?= =?us-ascii?q?MMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1?= =?us-ascii?q?oLejpB4Lelcu62/6v95HJYAhEmDWxbLNvIB6rsQjfq84ajJd4JK0s0BXJuHxIe?= =?us-ascii?q?+pXxWNsO12emgv369mz8pB+7Sleouot+MFcX6r0eaQ4VqFYAy89M28p/s3rtAL?= =?us-ascii?q?MQhWJ63ABT2gZiBtIAwzC7BHnQpf8tzbxu+Rh1CWGO8D9UKs5Uiq+4ah1VBDoi?= =?us-ascii?q?T8HNz8n/2HRlsxwl79QrBa4qxBi34LYfISZOfxjda3fYNwaX3JMUdpSWSJPDYy?= =?us-ascii?q?zYYsBAfcfM+tDtYbxu0EDoAGiCQSiBu7izCJDiH/s3a091uQsCRzI3BA+ENIQr?= =?us-ascii?q?nvfsdb6O7oIXuCz0KbH0zvCb/JK1jzg74XIaQwhru+SXb1ucMvc0lIvGB3fgVW?= =?us-ascii?q?Ls4DlIiuV2foLs2id9eZvS/+gi3M+pgx3vzOgydsihJPTiYIJ1lDL6z95wIAtK?= =?us-ascii?q?NC5R0N3f8CoHZhQuiyeNoZ7TcwsTmF0tSs+xLAItoK2cDUExZoo2hPSd/KKfoa?= =?us-ascii?q?V7h/gVeucIjN1iXZndb+9mxq/91WrxOP7VsmxyllKryxFn8HXtnAM2BzT8syHR?= =?us-ascii?q?eF7/ku73jaPzQ/T5+dZKk43jarWM4AtzqI0m5YJsknOHjX6lFvrgKKSbEkp9fa?= =?us-ascii?q?k5/z5brjnupORNYp5ig/xP6kshsCyBOU1Pw0BUmSH5eiwybju8E/9TbVEkvE7l?= =?us-ascii?q?6vUvI3UJcgGo6O5DRJa34k95Bu6ATem3tYVkmMBIVlYYhyIlZLpNEvLIP3gDfe?= =?us-ascii?q?wnVCskDBzyvDDJLLhA5HNImHakLf/YLpx8kBcxQUtwdxF6JJUDbYBIP33WkDvr?= =?us-ascii?q?tDXEhg5Mwmsz+bmDtVyyJ8eVHqRDqOFNK7eq1yF6+I1L+WSeYMYvCzxJvc76/L?= =?us-ascii?q?2iH82g14dfa2n3ZsNb3C4G+xrI16FYXXynNcOD2YLsxElTOP0klKCSiRfZ2uqX?= =?us-ascii?q?60i4DE7DpiqApneSYCwmLCBxju0HoVKZmBaDVCBCWvneJ+BW/cIcS6SJs5hkic?= =?us-ascii?q?YVbW6UI8g1RSutBfgxLZ9L+rU/DcYtZP529Rv6e3Tj0J6yTshBM2Y1ySJTnpot?= =?us-ascii?q?mIOXT4/mq5l5QR2zU7G2qxlidRZE8ZS7rVHSENyM4PE1ehSAMu0UQXbeNqNTBC?= =?us-ascii?q?rTsjiSS0gVt8qhtYIZUFgHd6vphTCxDaxRaQYnqfNGYQ59KSa0nTsdOhnzHOT7?= =?us-ascii?q?7UskVRucMdGM2arma90v1zIG4PXnlexjKujbuIBxCPL8iGOwXfY7xIQaxJ5Tai?= =?us-ascii?q?QBSNXXUDRt9msoxqaF9dG6JwiOwpFjNecc+5ENoevglJBS/Puft/ZZjDp849fL?= =?us-ascii?q?Q2Fz6jKcZLnfWNb0SnAWhFse+U75nuPLk4jHiqnpSTTACE8TTrS?= IronPort-Data: =?us-ascii?q?A9a23=3ArbO4UapfSHax6Csfv9l92hQnL9JeBmJvZBIvgKr?= =?us-ascii?q?LsJaIsI5as4F+vmNLXT/QOq3YYWGje98kYYW1pkkD7ZaEzdUwSgBl/yE2Zn8b8?= =?us-ascii?q?sCt6faxfh6hZXvKRiHgZBs6tJtGMoGowPjZ/xYwnz/1WlTahSQ6hfHgqobUUra?= =?us-ascii?q?eY3krHV48Ek/NtDo68wIHqt4w6TSGK1jV0T/Ci5W31G6Ng1aYAEpMg06wgE8HU?= =?us-ascii?q?MDJhd8tlgdWicanE7PpvyJ94Jo3fcldJpZjK2VeNrbSq+3rlNlV8o5FlirBBO9?= =?us-ascii?q?Jkp6jGqELarvbPAzLk2QPHqb+2F5NoSs91qt9P/0ZAatVo2/RzpYhlZMX7M32F?= =?us-ascii?q?V1B0q7kwIzxVzFDDyxgML9u47LOOj6iqcGVyQvLf2aEL/BGXR5tY9dJpY6bBkk?= =?us-ascii?q?XraBCQNwXVTiIjueyhba6UfVEndUmNMCtPYUFu3gmwyuxMBqMaYSbFv+MussBi?= =?us-ascii?q?W923tQUSK6YPZtIMC40OUyGPgkQb34JLLk7uMuoolj2VQFCjGyUgL5uuz2KiFU?= =?us-ascii?q?rxNABK/LQc92OANxLxwOW+jiA8GP+DRUXcteYzFK4HruXrrentUvGtEg6TubQG?= =?us-ascii?q?j9WbFyvKqg7DRQXUR6iv6D8hBLkHd1YLEMQ92wlqq1aGImDJjXid0XQnZJGlkd?= =?us-ascii?q?0txls/ykS8wyE0ezJ+wufAC4JQiMphBkOqpotXTJzvrOWt4qBONGs2YF5jVqG+?= =?us-ascii?q?76P6y6qNC4Ta2IOeEfoiCNtD8bL+OkOs/4Ecjqv/GNZQDE49fEcDg1mdBQDuog?= =?us-ascii?q?=3D?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3AbqnmoKM7nBvmSsBcTtSjsMiBIKoaSvp037BL?= =?us-ascii?q?7SFMoHNuGfBw+/rFoB1573HJYVQqNE3I8OroUJVoKkmyyXcB2/hyAV7UZniChI?= =?us-ascii?q?LHFuxfBPPZsl7d8nrFltJg6Q=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CIAQBaBbJhfyrbVdFaDhABAQsSDIIOC?= =?us-ascii?q?4EhMSyBJ1drhEeQZS6BFpUkhg0UgREDVAIJAQMBCwEBNQoCBAEBhQaDHQIdBwE?= =?us-ascii?q?EMgcOAQIEFQEBBQEBAQIBAwMEARMBAQ0LEAgyJIVoDYI1KQGDZhYLBh0BASYNB?= =?us-ascii?q?AFcAjYBBQEjDAYCAQESDIIESwGDFwEOoTKBBD2LMoExgQGCCAEBBoFCBYEUgxU?= =?us-ascii?q?JDYFaAwYJAQiBKIccDgGCf4QvHIFJRIEVJw+CPQVwgmMEgSkBEQIBgziCZZI2M?= =?us-ascii?q?UUPEykTRSpYBQkbMAotDZFcHI83nWGDSoE7iSeUKgYPBS2Db4t/hgqLCIV6TZY?= =?us-ascii?q?rH4xclBmFCQIKBwYQI4FFDYEQcE0lEzuCaVEZD1YBjUmDcoUUhQVjIzMCNgIGA?= =?us-ascii?q?QoBAQMJhWqJPF0BAQ?= X-IPAS-Result: =?us-ascii?q?A0CIAQBaBbJhfyrbVdFaDhABAQsSDIIOC4EhMSyBJ1drhEe?= =?us-ascii?q?QZS6BFpUkhg0UgREDVAIJAQMBCwEBNQoCBAEBhQaDHQIdBwEEMgcOAQIEFQEBB?= =?us-ascii?q?QEBAQIBAwMEARMBAQ0LEAgyJIVoDYI1KQGDZhYLBh0BASYNBAFcAjYBBQEjDAY?= =?us-ascii?q?CAQESDIIESwGDFwEOoTKBBD2LMoExgQGCCAEBBoFCBYEUgxUJDYFaAwYJAQiBK?= =?us-ascii?q?IccDgGCf4QvHIFJRIEVJw+CPQVwgmMEgSkBEQIBgziCZZI2MUUPEykTRSpYBQk?= =?us-ascii?q?bMAotDZFcHI83nWGDSoE7iSeUKgYPBS2Db4t/hgqLCIV6TZYrH4xclBmFCQIKB?= =?us-ascii?q?wYQI4FFDYEQcE0lEzuCaVEZD1YBjUmDcoUUhQVjIzMCNgIGAQoBAQMJhWqJPF0?= =?us-ascii?q?BAQ?= X-IronPort-AV: E=Sophos;i="5.88,192,1635199200"; d="scan'208,217";a="9736297" X-MGA-submission: =?us-ascii?q?MDEUmoYwwoRQn1aiE21VLZNRQJX66jUPBkCDqE?= =?us-ascii?q?lmadvzZ/v1oikcGAz28MM1zPASKw1lYu4R0M62zmdof0+VccmpoKwAqe?= =?us-ascii?q?xoTzBZivGgxltppM9pDOPdqaP7jHe2ijp9/SJLHqj65vXe6UtMCWiCbF?= =?us-ascii?q?MybsKYqeKR0PN6wWqBsWe/Bw=3D=3D?= Received: from mail-qv1-f42.google.com ([209.85.219.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 09 Dec 2021 14:35:24 +0100 Received: by mail-qv1-f42.google.com with SMTP id bu11so5155852qvb.0 for ; Thu, 09 Dec 2021 05:35:23 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=seas-upenn-edu.20210112.gappssmtp.com; s=20210112; h=message-id:date:mime-version:user-agent:content-language:from :subject:cc:to; bh=fZydSMA1CLs8s2AWmC1Bz0I3z1rSWD0mMblHcXJfKFg=; b=y5B0vBTLwdm/CZU2H1sonsCiEDRNdquYUpwxVn2S8k80ubQZ+sJfhN2f6hgrEsQgDx YEnlJVycqUfhvycAvuTmSig4HhWoVeLP/2rtr7t56EFSH8myO3CLw5ke58scNF2uj6We M/3tNJMXaDHXWQcWQLWU8bcYRl4IiIVgd71IoZbwK44ZC/XUGLIPlQuZsSwXAq40mVIX o4Cb76krb9yZSJPIJovxNILNYKC4noUbBZJk8Vog/UtEN9YRu4Iya/0E9kfllEdUjapg zT0E5DW1bcL8JMGUENMZZocdySwQ5mJYBGRWvwcMUADIPJPkdBctVs/l1K624rjrV3Fe ocGQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:message-id:date:mime-version:user-agent :content-language:from:subject:cc:to; bh=fZydSMA1CLs8s2AWmC1Bz0I3z1rSWD0mMblHcXJfKFg=; b=DfPAnXpaKTO4y97yroZl6+e4GcYZ0EdKuVbpZe4rTQ0JgDAlSekte+/xX9k0WS/MxM FkJaXH7dt6aVcoI3A2h9J8A86Nh1Gxc4W2HvV+BCro1yYY9p4dZTMwwsFKjG62I3NDd+ IjUhD6lIRSV3nyG4gfiDJ+e7FqctpBYxkFJoX11wJsseL3zIhk4ZgHXmw4+VGd4ZvCTH QamiIWEXVKkbefeYYAEjmBc4/IJJUEG1TmuaopM986f15YYeVl88Jp3XrND+puvTGzYp PhxHMaj908IAq++hz0vOhzlsNx/ppFasa8BPGsyK76aXpdWxaKm6zAo4ZsFxEEBK1sV/ bjrw== X-Gm-Message-State: AOAM532cpoEixU2mSXmofwX1DHjTy8NSB4aQWf57yP8Ilt+m1M0Lwp0g Qt0v+AiKKZjDizXFp+rk/s2vNz25pa42rPoM X-Google-Smtp-Source: ABdhPJzY744VD///9gHipRAtORqokP22tdKLSSHgKGjC3xUb1whI7vRuvM+poSANIfkwRedq7D9BGw== X-Received: by 2002:a05:6214:da9:: with SMTP id h9mr17293279qvh.2.1639056921503; Thu, 09 Dec 2021 05:35:21 -0800 (PST) Received: from ?IPV6:2607:f470:6:4001:79f0:71f1:fd4e:ff7a? ([2607:f470:6:4001:79f0:71f1:fd4e:ff7a]) by smtp.gmail.com with ESMTPSA id x16sm2911078qko.15.2021.12.09.05.35.20 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 09 Dec 2021 05:35:20 -0800 (PST) Content-Type: multipart/alternative; boundary="------------Ig0gue8T4GTeFNVdcW5MPFWR" Message-ID: <1264de38-faed-2eff-df99-ae9a40fb4614@seas.upenn.edu> Date: Thu, 9 Dec 2021 08:35:19 -0500 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0) Gecko/20100101 Thunderbird/91.4.0 Content-Language: en-US From: Steve Zdancewic Cc: Andrei Popescu , Lennart Beringer , Robbert Krebbers To: caml-list@inria.fr, coq-club@inria.fr, nuprl@cs.cornell.edu, types-announce@lists.seas.upenn.edu Subject: [Caml-list] Certified Programs and Proofs (CPP) 2022: Call for Participation Reply-To: Steve Zdancewic X-Loop: caml-list@inria.fr X-Sequence: 18623 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: This is a multi-part message in MIME format. --------------Ig0gue8T4GTeFNVdcW5MPFWR Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit * *** Call for Participation *** *** Certified Programs and Proofs (CPP 2022) ***  - Early registration deadline: 3 January 2022  - Getting a visa: https://popl22.sigplan.org/attending/visa-information  - Registration: https://popl22.sigplan.org/attending/registration  - Further reduced student participation fee: see below  - Accommodation: https://popl22.sigplan.org/venue/POPL-2022-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 2022 (https://popl22.sigplan.org/home/CPP-2022) will be held on 17-18 January 2022 and will be co-located with POPL 2022. CPP 2022 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 2022, CPP will take place as an in-person event at the Westin Philadelphia (99 South 17th Street at Liberty Place, 19103 Philadelphia), and will require attendees to provide proof of vaccination (details will be available soon). Authors who are unable to attend CPP in person will be able to present remotely. All talks will be recorded, and all recordings will be available either as a livestream or soon afterwards. For more information about this edition and the CPP series, please visit https://popl22.sigplan.org/home/CPP-2022 ### Invited talks * June Andronick (UNSW Sydney). The seL4 verification: the art and craft of proof and the reality of commercial support * Andrew W. Appel (Princeton). Coq’s vibrant ecosystem for verification engineering * Cesar Munoz (Currently at AWS, Formerly at NASA, USA). Structural Embeddings Revisited ### Accepted papers The list of accepted papers is available at https://popl22.sigplan.org/home/CPP-2022#event-overview ### Subsidized student registration To facilitate in-person participation of undergraduate and graduate students who require financial assistance, CPP 2022 offers the opportunity to register at a special reduced rate, determined on a case-by-case basis, and implemented using a special-purpose registration code on POPL's registration website. Students wishing to apply for such support may do so by sending mail to the CPP conference co-chairs (Beringer and Krebbers, see below for their email) preferably by December 24, 2021, with a brief description of their situation. Notifications will be sent out at most one week later; hence, students who cannot be supported will still have the opportunity to register at the publicly available reduced rate, which is available until January 3rd. Applications arriving after December 24th will be considered only in exceptional cases. Students who already receive registration support for PLMW or are supported by SIGPLAN PAC are not eligible. CPP's student support is made possible by to our generous industrial supporters: https://popl22.sigplan.org/home/CPP-2022 ### Contact For any questions please contact the chairs: Andrei Popescu (PC co-chair) Steve Zdancewic (PC co-chair) Lennart Beringer (conference co-chair) Robbert Krebbers (conference co-chair) * --------------Ig0gue8T4GTeFNVdcW5MPFWR Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

*** Call for Participation ***

*** Certified P= rograms and Proofs (CPP 2022) ***

=C2=A0- Early registration deadline: 3 January 2022

=C2=A0- Getting a visa: https://p= opl22.sigplan.org/attending/visa-information

=C2= =A0- Registration: https://popl22.sigplan.org/attend= ing/registration

=C2=A0- Further reduced stude= nt participation fee: see below

=C2=A0- Accommodat= ion: https://popl22.sigplan.org/venue/POPL-2022-venue=

Certified Programs and Proofs (CPP) is an international conf= erence on practical and theoretical topics in all areas that consider for= mal verification and certification as an essential paradigm for their wor= k. CPP spans areas of computer science, mathematics, logic, and education= =2E

CPP 2022 (https://popl22.sigplan.org/home/CPP-20= 22) will be held on 17-18 January 2022 and will be co-located with PO= PL 2022. CPP 2022 is sponsored by ACM SIGPLAN, in cooperation with ACM SI= GLOG, and supported by a diverse set of industrial sponsors.

Similarly to other events collocated with POPL 2022, CPP wil= l take place as an in-person event at the Westin Philadelphia (99 South 1= 7th Street at Liberty Place, 19103 Philadelphia), and will require attend= ees to provide proof of vaccination (details will be available soon). Aut= hors who are unable to attend CPP in person will be able to present remot= ely. All talks will be recorded, and all recordings will be available eit= her as a livestream or soon afterwards.

For more information about this edition and the CPP series, = please visit https://popl22.sigplan.org/home/CPP-2022

### Invited talks

* June Andronick (UNSW Sydney). The seL4 verification: the a= rt and craft of proof and the reality of commercial support

= * Andrew W. Appel (Princeton). Coq=E2=80=99s vibrant ecosystem = for verification engineering

* Cesar Munoz (Curren= tly at AWS, Formerly at NASA, USA). Structural Embeddings Revisited

### Accepted papers

The list of accepted papers is available at

https://popl22.sigplan.org/home/CPP-202= 2#event-overview

### Subsidized student registration

To facilitate in-person participation of undergraduate and g= raduate students who require financial assistance, CPP 2022 offers the op= portunity to register at a special reduced rate, determined on a case-by-= case basis, and implemented using a special-purpose registration code on = POPL's registration website. Students wishing to apply for such support m= ay do so by sending mail to the CPP conference co-chairs (Beringer and Kr= ebbers, see below for their email) preferably by December 24, 2021, with = a brief description of their situation. Notifications will be sent out at= most one week later; hence, students who cannot be supported will still = have the opportunity to register at the publicly available reduced rate, = which is available until January 3rd. Applications arriving after Decembe= r 24th will be considered only in exceptional cases. Students who already= receive registration support for PLMW or are supported by SIGPLAN PAC ar= e not eligible.

CPP's student support is made possible by to our generous in= dustrial supporters:

https://popl22.si= gplan.org/home/CPP-2022

### Contact

For any questions please contact the chairs:

Andrei Popescu <a.popescu@sheffield.ac.uk> (PC co-c= hair)

Steve Zdancewic <stevez@seas.upenn.edu>= ; (PC co-chair)

Lennart Beringer <eberi= nge@cs.princeton.edu> (conference co-chair)

Robbert Krebbers <mail@robbertkrebbers.nl> (conference co-ch= air)

--------------Ig0gue8T4GTeFNVdcW5MPFWR--