Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] PriSC 2021: call for participation and short t...

view this post on Zulip Email Gateway (Dec 04 2020 at 10:18):

From: PriSC PC Chairs <>
Principles of Secure Compilation (PriSC) 2021: Call for Participation
and Short Talks

tl;dr: a new exciting edition of PriSC is in the works! as usual, we've
a few slots for short talks, where speakers can spend a few minutes telling
about ongoing work and foster informal discussions; please do send us your
talks proposals!

Principles of Secure Compilation Workshop (PriSC 2021)

- Registration:
- Accepted talks available here:

- Invited speaker: Hugo Vincent (ARM)
- Call for short talks: see below
Deadline: January 11th 2021

The Workshop on Principles of Secure Compilation (PriSC) is an informal
workshop without proceedings. The goal is to bring together researchers
interested in secure compilation and to identify interesting research
and open challenges.

PriSC 2021 will be held on Saturday January 17th, 2021 online.
It will be co-located with POPL 2021, also online.

For more information about this edition and the PriSC series, please

Invited Speakers

Hugo Vincent (ARM)

Accepted papers

The list of accepted talks is available at

Call for Short Talks

We also have a short talks session, where participants get 5 minutes to
intriguing ideas, advertise ongoing work, etc. If you're interested in
giving a
short 5-minute talk, please submit an abstract. Any topic that could be of
interest to the emerging secure compilation community is in scope.
that provide a useful outside view or challenge the community are also

- Deadline: January 11th, 2021
- More details:

- Submit here:

Workshop summary

The emerging field of secure compilation aims to preserve security
properties of
programs when they have been compiled to low-level languages such as
where high-level abstractions don’t exist, and unsafe, unexpected
with libraries, other programs, the operating system and even the hardware
possible. For unsafe source languages like C, secure compilation requires
careful handling of undefined source-language behavior (like buffer
and double frees). Formally, secure compilation aims to protect high-level
language abstractions in compiled code, even against adversarial low-level
contexts, thus enabling sound reasoning about security in the source
language. A
complementary goal is to keep the compiled code efficient, often leveraging
hardware security features and advances in compiler design. Other necessary
components are identifying and formalizing properties that secure compilers
possess, devising efficient security mechanisms (both software and
and developing effective verification and proof techniques. Research in the
field thus puts together advances in compiler design, programming languages,
systems security, verification, and computer architecture.


For any questions please contact the workshop chairs, Jonathan Protzenko
( and Deian Stefan (

To make sure you receive PriSC announcements in the future please
subscribe to the following low-traffic mailing list:

Last updated: Jan 27 2022 at 20:19 UTC