The Coq mailing list

[Lennart Beringer <eberinge AT cs.princeton.edu>]

[ We are monitoring the COVID-19 situation and are in consultation
with the PLDI organizers concerning contingency plans. We expect this
will include the option to participate remotely, for both speakers and
audience members. ]

The

               REMS-DeepSpec 2020 workshop
      June 15-16, London UK (colocated with PLDI)
https://pldi20.sigplan.org/home/rems-deepspec-2020

invites proposals for presentations by researchers interested in the
semantics of and rigorous engineering methods for mainstream systems,
and in proof assistants to verify realistic software and hardware
stacks at scale.

REMS-DeepSpec 2020 is organized jointly by the EPSRC project REMS:
Rigorous Engineering for Mainstream Systems (UK) and the NSF
Expedition in Computing "The Science of Deep Specification" (US). It
will consist of in-depth presentations by members of the two projects,
invited talks by external experts, and general talks.

To foster exchange of ideas between members of the two projects and
researchers elsewhere, we now invite talk proposals, in the form of
abstracts of up to two pages in length (talks are expected to be 20-30
mins), to be submitted here:

https://remsdeepspec2020.hotcrp.com

We encourage submission by March 31 2020 AoE; later submissions will
be treated on a case-by-case basis.

Topics of interest include specification and verification of concrete
systems and their components, challenges in their validation,
composition, or semantic modeling, and lessons learned from applying
semantic techniques and proof assistants in industrial settings.

Proposals will undergo lightweight reviewing/selection by a
workshop committee, comprising (in addition to the organizers):

Magnus Myreen (Chalmers University, external)
Neel Krishnaswami (University of Cambridge, REMS)
Steve Zdancewic (University of Pennsylvania, DeepSpec)

There will be no formal proceedings but presenters will be encouraged
to make their presentations or abstracts available on the workshop web
page. 

We also plan to have a lightning talk session (talks of up to 5 mins
length), which will provide opportunities to present work-in-progress,
propose research ideas or collaborations, or to make short
announcements. Details will be announced shortly before the event.

Peter Sewell (University of Cambridge, REMS)
Lennart Beringer (Princeton University, DeepSpec)

REMS: https://www.cl.cam.ac.uk/~pes20/rems/
DeepSpec: https://deepspec.org/main