[TYPES/announce] Final CFP: Formal Methods and Programming Languages Track at CCS'24

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear colleagues,

I would like to draw your attention to the *Formal Methods and Programming
Languages (FM) **Track *at the *31st ACM Conference on Computer and
Communications Security (CCS'24)*, for which the second submission deadline
is coming up soon:

   - Second Review Cycle deadline: *April 29th, 2024 (updated!)*

The extended composition of the Program Committee on the FM track of
CCS'24 is as follows:

   - Adrien Koutsos (Inria Paris, France)
   - Alejandro Russo (Chalmers University, Sweden)
   - Bas Spitters (Aarhus University, Denmark)
   - Benjamin Gregoire (Inria Sophia-Antipolis, France)
   - Boris Köpf (Azure Research, Microsoft, Cambridge, UK)
   - Bruno Blanchet (Inria Paris, France)
   - Cas Cremers (CISPA Helmholtz Center for Information Security,
   Saarbrücken, Germany)
   - Clara Schneidewind (MPI-SP, Bochum, Germany)
   - Frank Piessens (KU Leuven, Belgium)
   - Frédéric Besson (Inria Rennes, France)
   - Guido Schmitz (Lancaster University Leipzig, Germany)
   - Ioana Boureanu (University of Surrey, UK)
   - Joshua Gancher (CMU, Pittsburgh, PA, USA)
   - Justin Hsu (Cornell University, Ithaca, NY, USA)
   - Limin Jia (CMU, Pittsburgh, PA, USA)
   - Marco Guarnieri (IMDEA Software Institute, Spain)
   - Mohsen Lesani (University of California, Riverside, CA, USA)
   - Stéphanie Delaune (CNRS, Rennes, France)
   - Swarn Priya (Virginia Tech, Blacksburg, VA, USA)

For more details please check the CCS'24 call for papers:
https://urldefense.com/v3/__https://www.sigsac.org/ccs/CCS2024/call-for/call-for-papers.html__;!!IBzWLUs!WkzwcOIm7nqeNvMqBM1RTM9Vvu7289rInPvD-yd73bVL9JaoxjpQQs_rIBI3YWWxyPdKR96THGA1wTcnt8nQFNKfPZOJy23UHhyD92E$
 

Kind regards,
Catalin Hritcu (MPI-SP, Bochum, Germany -- FM Track Chair)

[TYPES/announce] The Cornell, Maryland, Max Planck Pre-doctoral Research School 2023 (Call for participation)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Cornell, Maryland, Max Planck Pre-doctoral Research School 2023
Emerging Research Trends in Computer Science
https://urldefense.com/v3/__https://cmmrs.mpi-sws.org__;!!IBzWLUs!X5Tn8nnYrJa2ANGan4Jdj6Dg6HG62N7XbBuH3iykO7vpM-8icolCBOaEc5KZbjdeNbncyJ3fqfAdAaC_GzRi4Jk_3uE7upg-rQXiQkM$
 

August 6–13, 2023, Saarbrücken, Germany

Applications are requested from undergraduate students or Master's
students in computer science, computer engineering, or a related
discipline to The Cornell, Maryland, Max Planck Pre-doctoral Research
School. The 7th of this annual series of week-long schools will focus
on emerging research trends in computer science.

The small, select group of attendees will be exposed to
state-of-the-art research in computer science, have the opportunity
to interact one-on-one with internationally leading scientists from
three of the foremost academic institutions in research and higher
learning in the US and in Europe, and network with like-minded
students. They will get a sense of what it is like to pursue an
academic or an industrial research career in computer science and
have a head start when applying for graduate school.

For full consideration, applications should be received by February
28th, 2023. Travel and accommodation will be covered for accepted
students. Further information about the school and how to apply can
be found at 
https://urldefense.com/v3/__https://cmmrs.mpi-sws.org__;!!IBzWLUs!X5Tn8nnYrJa2ANGan4Jdj6Dg6HG62N7XbBuH3iykO7vpM-8icolCBOaEc5KZbjdeNbncyJ3fqfAdAaC_GzRi4Jk_3uE7upg-rQXiQkM$
 

[TYPES/announce] Professorship for System Security @ Ruhr Uni Bochum, Germany

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Horst Görtz Institute for IT Security (HGI) in Bochum, Germany is one
of the most renowned institutes in the field of IT Security in Europe. The
HGI comprises 26 faculty members, maintains extensive networks and has
produced numerous successful start-ups. HGI is home to the Cluster of
Excellence "CASA: Cyber Security in the Age of Large-Scale Adversaries",
funded with approximately 30 million euros. This outstanding environment
offers excellent working conditions in a highly topical and exciting field.
In addition, there is a very good working atmosphere in a young and diverse
group of researchers.


The *Faculty of Computer Science **at Ruhr-Universität Bochum* invites
applications for a *Professorship for System Security* (Open Rank: Tenured
Full Professorship or Associate / Assistant Professorship with Tenure Track).
Applicants should have an excellent track record in research and teaching
in at least one of the following areas:

   - System Security: Operating systems security, web security, distributed
   systems security, cloud computing security
   - Program analysis and analysis of security protocols
   - Machine learning security and privacy
   - Data-driven security and measurement studies
   - Privacy and anonymity
   - Applications of cryptography to real-world systems
   - Wireless security
   - Network security (intrusion and anomaly detection, network
   infrastructure security, DoS and countermeasures)
   - Strategic and economic aspects of real-world system security


We are looking for a scientist with an internationally visible research
profile who will complement existing research focus areas and actively
participate in the development of the newly founded Faculty for Computer
Science. We expect a willingness to cooperate with the Horst Görtz
Institute for IT Security and a leading role in current and planned
projects, especially in the Cluster of Excellence "CASA: Cyber Security in
the Age of Large-Scale Adversaries". The Max Planck Institute for
Cybersecurity and Privacy offers additional possibilities for
collaboration. There is also ample opportunity to interact with the
well-developed start-up community in the area of security and computer
science, including the Cube 5 IT Security incubator. The working language
is English. Fluent German is not a prerequisite for a successful engagement
at HGI.

The official job ad can be found here
.
Applications with the usual documents should be sent by 14.02.2023 to the
Vice Dean of the Faculty of Computer Science at the Ruhr-Universität
Bochum, Alexander May, e-mail: car...@casa.rub.de .

Further information can be found on our homepages at

*https://urldefense.com/v3/__https://www.informatik.rub.de/en__;!!IBzWLUs!VMbsvgTHIV_bWaC8awHxTgDOnUFBZrzzYyluDjTd_8dmXBXC8yOhvtTICBpLylwlFTzzLSrZi3ackW1mNr9Pv-5j7QoLONyIZMsYCMo$
 
**https://urldefense.com/v3/__https://casa.rub.de/en/__;!!IBzWLUs!VMbsvgTHIV_bWaC8awHxTgDOnUFBZrzzYyluDjTd_8dmXBXC8yOhvtTICBpLylwlFTzzLSrZi3ackW1mNr9Pv-5j7QoLONyI4U4wF_o$
 
* .

[TYPES/announce] Tenure-track Faculty Positions at Max Planck Institutes in Computer Science

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Max Planck Institutes in Computer Science invite applications for
tenure-track faculty in all areas of computer science. We expect to fill
several positions:
https://urldefense.com/v3/__https://www.cis.mpg.de/tenure-track-openings-at-max-planck-institutes-in-computer-science__;!!IBzWLUs!Rf025tfP0cGGzvzHLig7kcCMxFUDKgj1ldF5WbCEgdcnkdzSNUsfjlzXJmGoIOisDs1v2VhN9eYNqivp87vE5nt4LJLa-W4flsbeOMo$
 

A doctoral degree in computer science or related areas and an outstanding
research record are required. Successful candidates are expected to build a
team and pursue a highly visible research agenda, both independently and in
collaboration with other groups.

The institutes are part of a network of over 80 Max Planck Institutes,
Germany’s premier basic-research organisations. MPIs have an established
record of world-class, foundational research in the sciences, technology,
and the humanities. The institutes offer a unique environment that combines
the best aspects of a university department and a research laboratory:
Faculty enjoy full academic freedom, lead a team of doctoral students and
post-docs, and have the opportunity to teach university courses; at the
same time, they enjoy ongoing institutional funding in addition to
third-party funds, a technical infrastructure unrivaled for an academic
institution, as well as internationally competitive compensation.

We maintain an international and diverse work environment and seek
applications from outstanding researchers worldwide. The working language
is English; knowledge of the German language is not required for a
successful career at the institutes.


*Qualified candidates should apply on our application website
(apply.cis.mpg.de 
). Review of applications will
begin by December 1st, 2022.*
The Max Planck Society wishes to increase the number of women in those
areas where they are underrepresented. Women are therefore explicitly
encouraged to apply. The Max Planck Society is also committed to increasing
the number of employees with severe disabilities in its workforce.
Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended
to seven years based on a positive midterm evaluation in the fourth year. A
permanent contract can be awarded upon a successful tenure evaluation in
the sixth year.

[TYPES/announce] Research opportunities (internships, PhD positions, summer school) at Max Planck Institutes in Computer Science

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello everyone,

The Max Planck Institutes (MPIs) in Computer Science have several research
opportunities for strong students. Please help spread the word about them:

- Summer internships. *Deadline: 1st November 2022.*
https://urldefense.com/v3/__https://www.cis.mpg.de/internships/__;!!IBzWLUs!V_lwwYzaOEIIGpqkzL1Rj7cU5gesbSK4R41gjl2oh23nrTRCzl2eqaHTP0ftj1JUiA4mTeabmhVx4TtsIk9sOBLgVp6wZbrPZXmC3fg$
  

- Several PhD programs. Deadlines are announced on
https://urldefense.com/v3/__https://www.cis.mpg.de/graduate-programs__;!!IBzWLUs!V_lwwYzaOEIIGpqkzL1Rj7cU5gesbSK4R41gjl2oh23nrTRCzl2eqaHTP0ftj1JUiA4mTeabmhVx4TtsIk9sOBLgVp6wZbrPhZDrDRo$
   (*31st December 2022 for CS@Max
Planck 
* and IMPRS-TRUST).

- CMMRS, a 1-week on-site summer school to expose undergraduate and
Master's students to research. Deadline in January/February (TBA). Details
will be posted on 
https://urldefense.com/v3/__https://cmmrs.mpi-sws.org__;!!IBzWLUs!V_lwwYzaOEIIGpqkzL1Rj7cU5gesbSK4R41gjl2oh23nrTRCzl2eqaHTP0ftj1JUiA4mTeabmhVx4TtsIk9sOBLgVp6wZbrPS8bI7Mw$
  

About the MPIs: The participating institutes are part of a network of over
80 Max Planck Institutes, Germany’s premier basic-research organisations.
MPIs have an established record of world-class, foundational research in
the sciences, technology, and the humanities. They offer a unique
environment that combines the best aspects of a university department and a
research laboratory. All the programs listed above are highly selective,
and the participating institutes use English as their working language.

Kind regards,
Catalin

[TYPES/announce] Looking for PostDoc on Program Verification Techniques in F* and Coq

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello everyone,

A Postdoctoral Research position on Program Verification Techniques in F*
and Coq is available in my group at the Max Planck Institute for Security
and Privacy (MPI-SP). I am looking for candidates with an excellent
research track record and publications at top conferences (especially POPL
and ICFP). I am particularly looking for someone with research expertise
in: formal verification, proof assistants (particularly Coq and/or F*),
type theory, effects, monads, functional programming, parametricity,
programming language semantics, etc.

Candidates are expected to work collaboratively on topics of joint interest
and to help co-advise students, but can also dedicate some of their time to
their own independent projects.

MPI-SP 
<https://urldefense.com/v3/__https://www.mpi-sp.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkInaRNIX8$
  > is a relatively new research institute
founded in 2019 and is part of the Computer Science area of the Max Planck
Society 
<https://urldefense.com/v3/__https://www.cis.mpg.de__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcHrocUQ$
  >. We are located on the campus of Ruhr
University Bochum, in the Rhein-Ruhr
<https://urldefense.com/v3/__https://en.wikipedia.org/wiki/Rhine-Ruhr__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcZnxBUA$
  >metropolitan region, Germany’s
largest academic hub. The working language of MPI-SP is English, and no
knowledge of German is required for this job.

Do not hesitate to contact me if you are interested in this position! (or
to forward this to someone who could be interested)


Kind Regards,

Catalin Hritcu

https://urldefense.com/v3/__https://catalin-hritcu.github.io__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkITE9O7Dk$
  


PS: If you’re interested in this position, in a couple of days I can also
provide you with a large (non-exhaustive) list of potential research topics
on which we could work together. In the meantime, here are our recent
papers in this space:

Verifying non-terminating programs with IO in F*
<https://urldefense.com/v3/__https://theowinterhalter.github.io/res/iodiv-hope.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI6EQt480$
  >. Cezar-Constantin
Andrici, Théo Winterhalter, Cătălin Hrițcu, and Exequiel Rivas. To be
presented at the 10th ACM SIGPLAN Workshop on Higher-Order Programming with
Effects (HOPE 2022) 
<https://urldefense.com/v3/__https://icfp22.sigplan.org/home/hope-2022__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIyvSY11g$
  >. 11
September 2022 (today!).

Partial Dijkstra Monads for All
<https://urldefense.com/v3/__https://types22.inria.fr/files/2022/06/TYPES_2022_paper_18.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIXPfhwB8$
  >. Théo
Winterhalter, Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard,
Guido Martínez, and Exequiel Rivas. Presented at the 28th International
Conference on Types for Proofs and Programs (TYPES 2022)
<https://urldefense.com/v3/__https://types22.inria.fr/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIaWV_we4$
  >. 2022.

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
<https://urldefense.com/v3/__https://eprint.iacr.org/2021/397/20210526:113037__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIzBeih6I$
  >. Carmine Abate, Philipp
G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter,
Cătălin Hrițcu, Kenji Maillard, and Bas Spitters. In 34th IEEE Computer
Security Foundations Symposium (CSF)
<https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$
  >. 2021. Distinguished Paper
Award.

Dynamic IFC Theorems for Free! 
<https://urldefense.com/v3/__https://arxiv.org/abs/2005.04722__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIvXYiorI$
  >
Maximilian Algehed, Jean-Philippe Bernardy, and Cătălin Hrițcu. In 34nd
IEEE Computer Security Foundations Symposium (CSF)
<https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$
  >. 2021.

Hybrid Enforcement of IO Trace Properties
<https://url

[TYPES/announce] Professor positions at Ruhr University Bochum

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear colleagues,

The Faculty of Computer Science at Ruhr University Bochum
<https://urldefense.com/v3/__https://informatik.rub.de/en/__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTu0ITOaM$
 > (Germany) has several open full professor
positions
<https://urldefense.com/v3/__https://jobs.ruhr-uni-bochum.de/jobposting/586ac694779bd2eb1182486fc78c712a4ea899480__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTYMKx5KA$
 >,
which can also be filled by an assistant/associate professor with tenure
track to full professorship. The positions are part of a concerted effort
to foster collaborations with the recently established Max Planck Institute
for Security and Privacy (MPI-SP) 
<https://urldefense.com/v3/__https://www.mpi-sp.org__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTQyxBIgo$
 >. *Programming
Languages* and *Foundations of Computer Science* are two of the explicit
interest areas for these positions. The application deadline is 29 July
2022. More details below.

Kind regards,
Catalin Hritcu
Tenured Faculty at MPI-SP
and co-opted by the Faculty of Computer Science at Ruhr University Bochum

*Professorships in Computer Science*

The Faculty of Computer Science at Ruhr University Bochum
<https://urldefense.com/v3/__https://informatik.rub.de/en/__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTu0ITOaM$
 > (Germany) has several tenure-track or
tenured openings. The positions are part of a concerted effort to
strengthen the existing faculty and to foster collaborations with the
recently established Max Planck Institute for Security and Privacy (MPI-SP)
<https://urldefense.com/v3/__https://www.mpi-sp.org__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTQyxBIgo$
 >. We welcome outstanding applicants from all areas
of computer science, including *but not limited to*:

●   Foundations of Computer Science

●   Programming Languages

●   Software Engineering

●   Data Science (Data Mining, Machine Learning, Big Data)

●   Computer Architecture

Appointments will be made for full professorship, or as assistant/associate
professorship with tenure track to full professorship. Salaries and working
conditions are internationally competitive.

The Ruhr-University offers a vibrant environment for computer science
research. We offer opportunities for collaboration with MPI-SP
<https://urldefense.com/v3/__https://www.mpi-sp.org__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTQyxBIgo$
 > and the Cluster of Excellence “Cyber Security in
the Age of Large-Scale Adversaries (CASA)” 
<https://urldefense.com/v3/__https://casa.rub.de/en/__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTL_v4FqQ$
 >. There
is also ample opportunity to interact with Bochum’s well-developed start-up
community, which includes a dedicated incubator. Our working language is
English, knowledge of German is not required. Ruhr-University Bochum offers
a family-friendly environment.

Candidates are expected to show:

●   An interest and commitment to building up the computer science
faculty,

●   the willingness to engage in interdisciplinary scientific work, and

●   leadership experience.

Candidates are asked to apply with the following documents: curriculum
vitae, research and teaching statement, copies of diplomas (in official
English or German translation), list of publications, and list of own
third-party funding.

Applications in PDF format should be sent by July 29, 2022, to the Dean of
the Faculty of Computer Science at Ruhr-University Bochum, Alexander May,
e-mail: car...@casa.rub.de .

The official job ad can be found here
https://urldefense.com/v3/__https://jobs.ruhr-uni-bochum.de/jobposting/586ac694779bd2eb1182486fc78c712a4ea899480?ref=homepage__;!!IBzWLUs!Q7cb-7bRFbAfmBSphbeqTcuahYY8UeSxCQPCtuUA2bVY5l75_lGr1rYM1ACMcDNHIJwf8YPIfrrb-htO0rVUPZa_Q86-EspTY3AcunQ$
 

[TYPES/announce] CS@max planck doctoral program applications by 31 December

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Looking for a top PhD program in English that you can start after BSc or MSc?

CS@max planck is a highly selective doctoral program that grants
admitted students full financial support to pursue research in the
broad area of computer and information science, with faculty at Max
Planck Institutes and some of the best German universities.

To qualify for the program, students must hold a Bachelor’s or
Master’s degree in computer science (or a related field) and have an
outstanding academic record. We especially encourage applications from
students who wish to explore research across the CS spectrum before
committing to a topic and advisor.

For more information about CS@max planck, see here:
https://www.cis.mpg.de/graduate-programs/cs-max-planck

The next upcoming application deadline is 31 December 2020.

[TYPES/announce] Tenure-track Openings at Max Planck Institutes in Computer Science

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Max Planck Institutes for Informatics 
 (Saarbrücken), Software Systems  (Saarbrücken
and Kaiserslautern), and Security and Privacy
 (Bochum),
invite applications for tenure-track faculty in all areas of computer
science. We expect to fill several positions.

A doctoral degree in computer science or related areas and an outstanding
research record are required. Successful candidates are expected to build a
team and pursue a highly visible research agenda, both independently and in
collaboration with other groups.

The institutes are part of a network of over 80 Max Planck Institutes,
Germany’s premier basic-research organisations. MPIs have an established
record of world-class, foundational research in the sciences, technology,
and the humanities. The institutes offer a unique environment that combines
the best aspects of a university department and a research laboratory:
Faculty enjoy full academic freedom, lead a team of doctoral students and
post-docs, and have the opportunity to teach university courses; at the
same time, they enjoy ongoing institutional funding in addition to
third-party funds, a technical infrastructure unrivaled for an academic
institution, as well as internationally competitive compensation.

We maintain an international and diverse work environment and seek
applications from outstanding researchers worldwide. The working language
is English; knowledge of the German language is not required for a
successful career at the institutes.

Qualified candidates should apply on our application website (
apply.cis.mpg.de). To receive full consideration, applications should be
received by *December 15th, 2020*.

The Max Planck Society wishes to increase the number of women in those
areas where they are underrepresented. Women are therefore explicitly
encouraged to apply. The Max Planck Society is also committed to increasing
the number of employees with severe disabilities in its workforce.
Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended
to seven years based on a positive midterm evaluation in the fourth year. A
permanent contract can be awarded upon a successful tenure evaluation in
the sixth year.

[TYPES/announce] Fwd: Second Call for Presentations: PriSC 2021 @ POPL 2021

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

I'm forwarding the following message on behalf of the PriSC 2021 chairs:


-- Forwarded message -
From: Jonathan Protzenko 
Date: Tue, Oct 27, 2020 at 8:49 PM
Subject: Second Call for Presentations: PriSC 2021 @ POPL 2021


(Apologies if you're getting this email multiple times.)

Short version: PriSC is a fun, welcoming and exciting venue. Share
updates, ideas, thoughts or send students for a friendly gathering that
may lead to future collaborations and ideas. Submit now!

All details are on the PriSC site
 and in this email.


Call for Presentations: PriSC 2021 @ POPL 2021


The emerging field of secure compilation aims to preserve security
properties of programs when they have been compiled to low-level
languages such as assembly, where high-level abstractions don’t exist,
and unsafe, unexpected interactions with libraries, other programs,
the operating system and even the hardware are possible. For unsafe
source languages like C, secure compilation requires careful handling
of undefined source-language behavior (like buffer overflows 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 new hardware security features and
advances in compiler design. Other necessary components are
identifying and formalizing properties that secure compilers must
possess, devising efficient security mechanisms (both software and
hardware), 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.

5th Workshop on Principles of Secure Compilation (PriSC 2021)
=

The Workshop on Principles of Secure Compilation (PriSC) is a
relatively new, informal 1-day workshop without any proceedings. The
goal is to bring together researchers interested in secure compilation
and to identify interesting research directions and open challenges.
The 5th edition of PriSC will be held on January 17 online,
together with the ACM SIGPLAN Symposium on Principles of
Programming Languages (POPL), 2021.

Important Dates
===

* Fri 30 Oct 2020: Submission deadline
* Wed 25 Nov 2020: Notification
* Sun 17 Jan 2021: Workshop

Presentation Proposals and Attending the Workshop
=

Anyone interested in presenting at the workshop should submit an
extended abstract (up to 2 pages, details below) covering past,
ongoing, or future work. Any topic that could be of interest to secure
compilation is in scope. Secure compilation should be interpreted very
broadly to include any work in security, programming languages,
architecture, systems or their combination that can be leveraged to
preserve security properties of programs when they are compiled or to
eliminate low-level vulnerabilities.  Presentations that provide a
useful outside view or challenge the community are also welcome. This
includes presentations on new attack vectors such as
microarchitectural side-channels, whose defenses could benefit from
compiler techniques.

Specific topics of interest include but are not limited to:

* Attacker models for secure compiler chains.
* Secure compiler properties: fully abstract compilation and similar
properties, memory safety, control-flow integrity, preservation of
safety, information flow and other (hyper-)properties against
adversarial contexts, secure multi-language interoperability.
* Secure interaction between different programming languages: foreign
function interfaces, gradual types, securely combining different
memory management strategies.
* Enforcement mechanisms and low-level security primitives: static
checking, program verification, typed assembly languages, reference
monitoring, program rewriting, software-based isolation/hiding
techniques (SFI, crypto-based, randomization-based,
OS/hypervisor-based), security-oriented architectural features such as
Intel’s SGX, MPX and MPK, capability machines, side-channel defenses,
object capabilities.
* Experimental evaluation and applications of secure compilers.
* Proof methods relevant to compilation: (bi)simulation, logical
relations, game semantics, trace semantics, multi-language semantics,
embedded interpreters.
* Formal verification of secure compilation chains (protection
mechanisms, compilers, linkers, loaders), machine-checked proofs,
translation validation, property-based testing.

Guidelines for Submitting Extended 

[TYPES/announce] Junior Research Group Leader positions at MPI for Security and Privacy

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Max Planck Institute for Security and Privacy in Bochum, Germany is
inviting applications for Junior Research Group Leader positions

Our Junior Research Group program offers young scientists the opportunity
to develop their own independent research program. We welcome applicants
from all areas of security and privacy, including foundations, formal
methods, cryptography, software and hardware security, as well as human and
other interdisciplinary aspects (e.g., computer science and psychology,
economy, law, policy, ethics, etc). The position is funded for 5 years.
Applicants must have completed a doctoral degree in computer science or
related areas and must have demonstrated outstanding research vision, and
potential to successfully lead a research group. Successful candidates are
expected to build a highly visible research agenda, to mentor Ph.D.
students, and to participate in collaborative projects.

The Max Planck Institute for Security and Privacy (https://www.mpi-sp.org)
is located in Bochum, Germany. We maintain an open, international, and
diverse work environment and seek applications from outstanding researchers
regardless of national origin. Our working language is English. We
collaborate with several major research institutions worldwide and have
high international visibility. We offer competitive salaries and support
for Ph.D. students, as well as generous travel, administrative, and
technical support.

Please apply at https://apply.cis.mpg.de/register/mpispjrgl
You need to send your CV, a research plan, an optional teaching statement,
and 3-5 references. Reviewing of applications will start immediately and
will continue until the positions are filled. The expected starting date
for the position is Fall 2020, open to negotiations. Informal inquiries can
be addressed to applications-j...@mpi-sp.org

[TYPES/announce] CFP for Certified Programs and Proofs (CPP 2020)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

## CFP for Certified Programs and Proofs (CPP 2020) ##

Certified Programs and Proofs (CPP) is an international conference on
practical and theoretical topics in all areas that consider
certification as an essential paradigm for their work. Certification
here means formal, mechanized verification of some sort, preferably
with the production of independently checkable certificates.
CPP spans areas of computer science, mathematics, logic, and education.

CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020. CPP 2020 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

For more information about this edition and the CPP series please visit:
https://popl20.sigplan.org/home/CPP-2020

### News

- Submission guideline news: **lightweight double-blind reviewing process**
  and **unrestricted appendices** that don't count against the page limit

- Delighted to announce that the **invited speakers** for CPP 2020 will be:
  Adam Chlipala (MIT CSAIL) and Grigore Rosu (UIUC and Runtime Verification)

- CPP 2020 will also host the **POPLmark 15 Year Retrospective Panel**

### Important Dates

   - Abstract Deadline: 16 October 2019 at 23:59 AoE (UTC-12h)
   - Paper Submission Deadline: 21 October 2019 at 23:59 AoE (UTC-12h)
   - Notification: 27 November 2019
   - Camera Ready Deadline: 20 December 2019
   - Conference: 20 - 21 January 2020

Deadlines expire at the end of the day, anywhere on earth. Abstract
and submission deadlines are tight and there will be **no extensions**.

### Topics of Interest

We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interests to CPP:

   - certified or certifying programming, compilation, linking, OS
 kernels, runtime systems, and security monitors;
   - certified mathematical libraries and mathematical theorems;
   - proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL,
 HOL-Light, 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 logical frameworks;
   - higher-order logics, dependent type theory, proof theory,
 logical 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,
 polynomial systems, SAT, SMT, and unification in algebras of interest;
   - certificates for semi-decision procedures, including equality,
 first-order logic, and higher-order unification;
   - certificates for program termination;
   - formal models of computation;
   - mechanized (un)decidability and computational complexity proofs;
   - user interfaces for proof assistants and theorem provers;
   - original formal proofs of known results in math or computer science;
   - teaching mathematics and computer science with proof assistants.

### Program Committee Members

   - Jasmin Christian Blanchette (VU Amsterdam, Netherlands -- co-chair)
   - Catalin Hritcu (Inria Paris, France -- co-chair)
   - Nada Amin (Harvard University - USA)
   - Jesús María Aransay Azofra (Universidad de La Rioja - Spain)
   - Mauricio Ayala-Rincon (Universidade de Brasilia - Brazil)
   - Liron Cohen (Cornell University - USA)
   - Dominique Devriese (Vrije Universiteit Brussel - Belgium)
   - Jean-Christophe Filliâtre (CNRS - France)
   - Adam Grabowski (University of Bialystok - Poland)
   - Warren Hunt (University of Texas - USA)
   - Ori Lahav (Tel Aviv University - Israel)
   - Peter Lammich (The University of Manchester - UK)
   - Dominique Larchey-Wendling (Univ. de Lorraine, CNRS, LORIA - France)
   - Hongjin Liang (Nanjing University - China)
   - Assia Mahboubi (Inria and VU Amsterdam - France)
   - Cesar Munoz (NASA - USA)
   - Vivek Nigam (fortiss GmbH - Germany)
   - Benjamin Pierce (University of Pennsylvania - USA)
   - Vincent Rahli (University of Luxembourg, SnT - Luxembourg)
   - Christine Rizkallah (UNSW Sydney - Australia)
   - Ilya Sergey (Yale-NUS College and National University of Singapore)
   - Kathrin Stark (Saarland University - Germany)
   - Nikhil Swamy (Microsoft Research - USA)
   - Nicolas Tabareau (Inria - France)
   - Dmitriy Traytel (ETH Zürich - Switzerland)
   - Floris van Doorn (University of Pittsburgh - USA)
   - Akihisa Yamada (National Institute of Informatics - Japan)
   - Roberto Zunino (University of Trento - Italy)

### Submission Guidelines

Prior to the paper submission deadline

[TYPES/announce] CPP 2020: Call for Sponsors

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)
covers all areas that consider formal verification as an essential paradigm for
their work. CPP spans areas of computer science, mathematics, logic, and
education and brings together 100+ researchers and practitioners to present the
latest developments in formal verification. More information about CPP at:
https://popl20.sigplan.org/home/CPP-2020

CPP welcomes corporate donations to help maintain and improve the overall
experience at the conference. The money we get from corporate sponsors will
generally be used to subsidize student attendance (e.g., registration weaving,
which generally increases student participation), cover the travel costs of
invited speakers, and pay for the conference dinner. This will also allow us
explore new ideas such as adding a distinguished paper award, or covering the
fees that would make CPP open access for everyone.

### CPP Support Levels

 Bronze -- Suggested donation $1000
- your name and logo prominently displayed on the CPP website
- acknowledgment in the CPP PC chair's statement for the proceedings
- big thank you in the CPP PC chair's report talk

 Silver -- Suggested donation $2500
- as above plus:
- an opportunity to display printed materials or branded merchandise
  (e.g., t-shirts, but **no** coffee containers please) on a joint table in
  the CPP conference room, or, space permitting, next to the entrance door
- one complementary registration to CPP (20-21 January 2019)

 Gold -- Suggested donation $5000
- as above plus:
- acknowledgement as a sponsor of the CPP keynote talks
- a banner on stage carrying the supporter's logo (it is the company's
  responsibility to produce and bring this to the conference)
- table/booth-like space at CPP where, if you wish, you can display publicity
  material, distribute handouts, talk to people, or demo software
  (for the duration of CPP, 20-21 January 2019).
- an opportunity to also display printed materials at the registration desk
  (which is joint with POPL)
- two complementary registrations to CPP (20-21 January 2019)
- other arrangements are possible based on your needs and interests
  (subject to ACM restrictions on commercial involvement)

 Platinum -- Suggested donation $1
- as above plus:
- an opportunity to be the sponsor of the CPP conference dinner;
  a representative from the company will be granted 10 minutes
  at the beginning of the dinner to address the attendees
- an opportunity to include branded merchandise in all POPL and CPP
  participant's swag bag, such as a flyer, for example, if desired
- three complementary registrations to CPP (20-21 January 2019)
- other arrangements are possible based on your needs and interests
  (subject to ACM restrictions on commercial involvement)

### Contact

Questions about how to contribute to CPP may be directed to
catalin.hri...@gmail.com

[TYPES/announce] 1st CFP for Certified Programs and Proofs (CPP 2020)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

**1st CFP for Certified Programs and Proofs (CPP 2020)**

Certified Programs and Proofs (CPP) is an international conference on
practical and theoretical topics in all areas that consider
certification as an essential paradigm for their work. Certification
here means formal, mechanized verification of some sort, preferably
with the production of independently checkable certificates.
CPP spans areas of computer science, mathematics, logics, and education.

CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020. CPP 2020 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

For more information about this edition and the CPP series please visit:
https://popl20.sigplan.org/home/CPP-2020

### Important Dates

   - Abstract Deadline: 16 October 2019 at 23:59 AoE (UTC-12h)
   - Paper Submission Deadline: 21 October 2019 at 23:59 AoE (UTC-12h)
   - Conference: 20 - 21 January 2020

### Topics of Interest

We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interests to CPP:

   - certified or certifying programming, compilation, linking, OS
 kernels, runtime systems, and security monitors;
   - certified mathematical libraries and mathematical theorems;
   - proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL,
 HOL-Light, 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 logical frameworks;
   - higher-order logics, dependent type theory, proof theory,
 logical 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,
 polynomial systems, SAT, SMT, and unification in algebras of interest;
   - certificates for semi-decision procedures, including equality,
 first-order logic, and higher-order unification;
   - certificates for program termination;
   - formal models of computation;
   - mechanized (un)decidability and computational complexity proofs;
   - user interfaces for proof assistants and theorem provers
   - teaching mathematics and computer science with proof assistants.

### Program Committee Members

   - Nada Amin (Harvard University - USA)
   - Jesús María Aransay Azofra (Universidad de La Rioja - Spain)
   - Mauricio Ayala-Rincon (Universidade de Brasilia - Brazil)
   - Liron Cohen (Cornell University - USA)
   - Dominique Devriese (Vrije Universiteit Brussel - Belgium)
   - Jean-Christophe Filliâtre (CNRS - France)
   - Adam Grabowski (University of Bialystok - Poland)
   - Warren Hunt (University of Texas - USA)
   - Ori Lahav (Tel Aviv University - Israel)
   - Peter Lammich (The University of Manchester - UK)
   - Dominique Larchey-Wendling (Univ. de Lorraine, CNRS, LORIA - France)
   - Hongjin Liang (Nanjing University - China)
   - Assia Mahboubi (Inria and VU Amsterdam - France)
   - Cesar Munoz (NASA - USA)
   - Vivek Nigam (fortiss GmbH - Germany)
   - Benjamin Pierce (University of Pennsylvania - USA)
   - Vincent Rahli (University of Luxembourg, SnT - Luxembourg)
   - Christine Rizkallah (UNSW Sydney - Australia)
   - Ilya Sergey (Yale-NUS College and National University of Singapore)
   - Kathrin Stark (Saarland University - Germany)
   - Nikhil Swamy (Microsoft Research - USA)
   - Nicolas Tabareau (Inria - France)
   - Dmitriy Traytel (ETH Zürich - Switzerland)
   - Floris van Doorn (University of Pittsburgh - USA)
   - Akihisa Yamada (National Institute of Informatics - Japan)
   - Roberto Zunino (University of Trento - Italy)

### Submission Guidelines

Submission guidelines will be made available in due course.

### Contact

For any questions please contact the two PC chairs:
Jasmin Christian Blanchette ,
Catalin Hritcu 

[TYPES/announce] PostDoc position at Inria Paris on Formally Secure Compilation in Coq

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello,

A PostDoc position is available in my group at Inria Paris on Formally
Secure Compilation in Coq (https://secure-compilation.github.io).
I am seeking outstanding candidates with a strong, internationally
competitive research track record. Particularly interesting for us is
research expertise in:
- formal verification in the Coq proof assistant
  and verified compilation in particular (e.g. CompCert)
- security foundations, e.g., reference monitoring,
  hyperproperties, noninterference
Here are some (non-exhaustive) lists of potential research topics:
http://prosecco.gforge.inria.fr/personal/hritcu/temp/habil/catalin_habil.pdf#page=80

Candidates are expected to work collaboratively on project-relevant
topics and help advise students, but can also dedicate some of their
time to their own independent projects. For exceptional candidates
with enough experience we can also discuss about Starting Researcher
positions, who can propose and follow their own research agenda and be
fairly independent. Our team can also support such exceptional
candidates for permanent Researcher positions funded and awarded
competitively by Inria. Further details about these various positions
are available at https://secure-compilation.github.io/#positions

Do not hesitate to contact me if you are interested!

Regards,
Catalin

[TYPES/announce] PostDoc positions at Inria Paris on F* and on Formally Secure Compilation

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello everyone,

2 PostDoc positions are available in my group at Inria Paris on the
F* and ERC SECOMP projects. I am seeking exceptional candidates
with a strong, internationally competitive research track record.

On F* (https://www.fstar-lang.org/), I am looking for someone with
research expertise in: programming language semantics, dependent
types, type theory, effects, monads, mechanized metatheory, functional
programming, formal verification. Here is a (non-exhaustive) list of
potential research topics on which we could work:
http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2018/fstar-topics.pdf

On ERC SECOMP (https://secure-compilation.github.io/), I am
particularly looking for someone with expertise in:
- formal verification in a proof assistant like Coq
  and verified compilation in particular
- security foundations, e.g., reference monitoring,
  hyperproperties, noninterference
Here is a (non-exhaustive) list of potential research topics:
http://prosecco.gforge.inria.fr/personal/hritcu/temp/habil/catalin_habil.pdf#page=80

Candidates are expected to work collaboratively on project-relevant
topics and help advise students, but can also dedicate some of their
time to their own independent projects. For exceptional candidates
with enough experience we can also discuss about Starting Researcher
positions, who can propose and follow their own research agenda and be
fairly independent. Our team can also support such exceptional
candidates for permanent Researcher positions funded and awarded
competitively by Inria. Further details about these various positions
are available at https://secure-compilation.github.io/#positions

Do not hesitate to contact me if you are interested in joining the team!

Kind Regards,
Catalin

[TYPES/announce] PostDoc Position on Formally Secure Compilation at Inria Paris

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A Postdoctoral Researcher position is available on my secure
compilation project at Inria Paris. The project is aimed at building
the first formally secure compilation chains for realistic programming
languages like C. Such compiler chains will ensure that high-level
abstractions cannot be violated even when interacting with untrusted
low-level code or when some program components were compromised.

I am seeking exceptional candidates with a strong, internationally
competitive track record of research in programming languages, formal
verification, or security. Particularly interesting areas include:

- formal verification in a proof assistant like Coq and
  verified compilation in particular

- security foundations, e.g., reference monitoring, hyperproperties,
  noninterference, fully abstract translations

Candidates are expected to work collaboratively and help advise students.

Please see the project web page (https://secure-compilation.github.io)
for more details about the project and about such open positions.
Do not hesitate to contact me if you are interested in joining the team!

Best Regards,
Catalin Hritcu

[TYPES/announce] Call for Short Talks on Secure Compilation (PriSC Workshop @ POPL'18)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

===
Call for Short Talks on Secure Compilation (PriSC Workshop @ POPL'18)
===

Do not miss the chance to submit short talks on your cutting-edge
secure compilation research. Submission deadline is 14 December 2017.
More information below.


==
Important Dates
==

  Short talk submission deadline:14 December 2017, AoE
  Short talk notification:   18 December 2017
  PriSC Workshop takes place:13 January 2018


==
Scope of PriSC Short Talks Session
==

In the short talks session of PriSC, participants get 5 minutes to
present intriguing ideas, advertise ongoing work, etc.  Anyone
interested in giving a short 5-minute talk should submit an
abstract. Any topic that could be of interest to the emerging secure
compilation community is in scope. Presentations that provide a useful
outside view or challenge the community are also welcome.

Topics of interest include but are **not** limited to:

- attacker models for secure compiler chains

- secure compilation properties: full abstraction, memory safety,
control-flow integrity, preserving non-interference or
(hyper-)properties against adversarial contexts,
secure multi-language interoperability

- enforcement mechanisms: static checking, program verification,
reference monitoring, program rewriting, software fault isolation,
system-level protection, secure hardware, crypto, randomization

- experimental evaluation and applications of secure compilation

- proof methods: (bi)simulation, logical relations, game semantics,
multi-language semantics, embedded interpreters

- formal verification of secure compilation chain (protection
mechanisms, compilers, linkers, loaders), machine-checked proofs,
translation validation, property-based testing


==
Guidelines for Submitting Short Talk Abstracts
==

Abstracts should be submitted in text format and are not anonymous

Giving a talk at the workshop does not preclude publication elsewhere.

Please submit your abstracts at https://prisc18short.hotcrp.com

For questions about the short talks please contact the Program Chair.


==
2nd Workshop on Principles of Secure Compilation (PriSC 2018)
==

The Workshop on Principles of Secure Compilation (PriSC) is a new
informal 1-day workshop without any proceedings. The goal is to
identify interesting research directions and open challenges and to
bring together researchers interested in secure compilation.

The 2nd PriSC edition will be held on Saturday, 13 January 2018, in
Los Angeles, together with the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL).

More information including the workshop program available at
http://popl18.sigplan.org/track/prisc-2018


==
Participation and Registration
==

PriSC will be held at the POPL'18 venue (Omni Hotel LA).
To participate, please register through the POPL registration system:
https://popl18.sigplan.org/attending/Registration


==
Program Committee
==

Program Chair
  Catalin Hritcu   Inria Paris

Members
  Amal Ahmed   Inria Paris and Northeastern University
  Lars BirkedalAarhus University
  Dominique Devriese   KU Leuven
  Cédric Fournet   Microsoft Research
  Deepak Garg  MPI-SWS
  Xavier Leroy Inria Paris
  David NaumannStevens Institute of Technology
  Marco Patrignani MPI-SWS
  Frank Piessens   KU Leuven
  Tamara Rezk  Inria Sophia Antipolis
  Nikhil Swamy Microsoft Research


==
Organizing Committee
==

  Amal Ahmed   Inria Paris and Northeastern University
  Dominique Devriese   KU Leuven
  Deepak Garg  MPI-SWS
  Catalin Hritcu   Inria Paris
  Marco Patrignani MPI-SWS
  Tamara Rezk  Inria Sophia Antipolis

[TYPES/announce] Call for Participation for Secure Compilation Workshop (PriSC @ POPL'18)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

===
Call for Participation for Secure Compilation Workshop (PriSC @ POPL'18)
===

Secure compilation is an emerging field that puts together advances in
programming languages, security, verification, systems, compilers, and
hardware architectures in order to devise secure compiler chains that
eliminate many of today's low-level vulnerabilities. Secure
compilation aims to protect high-level language abstractions in
compiled code, even against adversarial low-level contexts, and to
allow sound reasoning about security in the source language. The
emerging secure compilation community aims to achieve this by:
identifying and formalizing properties that secure compilers must
possess; devising efficient enforcement mechanisms; and developing
effective verification and proof techniques.


==
2nd Workshop on Principles of Secure Compilation (PriSC 2018)
==

The Workshop on Principles of Secure Compilation (PriSC) is a new
informal 1-day workshop without any proceedings. The goal is to
identify interesting research directions and open challenges and to
bring together researchers interested in secure compilation.

The 2nd PriSC edition will be held on Saturday, 13 January 2018, in
Los Angeles, together with the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL).

More information at http://popl18.sigplan.org/track/prisc-2018


==
Important Dates
==

  POPL early registration deadline:  10 December 2017
  Short talk submission deadline:14 December 2017, AoE
  Short talk notification:   18 December 2017
  PriSC Workshop takes place:13 January 2018

Do not miss the chance to submit short talks on your cutting-edge
research. More information below.


==
Invited Talk
==

Challenges For Compiler-backed Security: From Sanitizer to Mitigation.
  Mathias Payer (Purdue University, https://nebelwelt.net/)


==
Accepted Presentations
==

Building Secure SGX Enclaves using F*, C/C++ and X64.
  Anitha Gollamudi, Cédric Fournet.

Constant-time WebAssembly.  John Renner, Sunjay Cauligi, Deian Stefan.

Enforcing Well-bracketed Control Flow and Stack Encapsulation using
  Linear Capabilities.  Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Formally Secure Compilation of Unsafe Low-Level Components.
  Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Ana Nora Evans,
  Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach

Linear capabilities for modular fully-abstract compilation of verified code.
  Thomas Van Strydonck, Dominique Devriese, Frank Piessens.

On Compositional Compiler Correctness and Fully Abstract Compilation.
  Daniel Patterson, Amal Ahmed.

Per-Thread Compositional Compilation for Confidentiality-Preserving
Concurrent Programs.  Robert Sison.

Robust Hyperproperty Preservation for Secure Compilation.  Deepak Garg,
  Catalin Hritcu, Marco Patrignani, Marco Stronati, David Swasey.

Secure Compilation in a Production Environment. Vijay D'Silva.

Type-Theoretic Galois Connections.
  Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter


==
Participation and Registration
==

PriSC will be held on Saturday, 13 Jan 2018 at the POPL'18 venue
(Omni Hotel LA). To participate, please register through the POPL
registration system: https://popl18.sigplan.org/attending/Registration

POPL early registration rate ends on 10 December 2017.


==
Call for Short Talks
==

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

Topics of interest include but are **not** limited to:

- attacker models for secure compiler chains

- secure compilation properties: full abstraction, memory safety

[TYPES/announce] Deadline extended for Secure Compilation workshop (PriSC @ POPL'18)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The PriSC'18 deadline has been extended by 1 week to the end of
Wednesday, 25 October 2017, AoE.

===
Call for Presentations on Secure Compilation (PriSC Workshop @ POPL'18)
===

Secure compilation is an emerging field that puts together advances in
programming languages, security, verification, systems, compilers, and
hardware architectures in order to devise secure compiler chains that
eliminate many of today's low-level vulnerabilities. Secure
compilation aims to protect high-level language abstractions in
compiled code, even against adversarial low-level contexts, and to
allow sound reasoning about security in the source language. The
emerging secure compilation community aims to achieve this by:
identifying and formalizing properties that secure compilers must
possess; devising efficient enforcement mechanisms; and developing
effective verification and proof techniques.


==
2nd Workshop on Principles of Secure Compilation (PriSC 2018)
==

The Workshop on Principles of Secure Compilation (PriSC) is a new
informal 1-day workshop without any proceedings. The goal is to
identify interesting research directions and open challenges and to
bring together researchers interested in secure compilation.

The 2nd PriSC edition will be held on Saturday, 13 January 2018, in
Los Angeles, together with the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL).

More information at http://popl18.sigplan.org/track/prisc-2018


==
Important Dates
==

  Presentation proposal submission deadline:  25 October 2017, AoE
  Presentation proposal notification: 15 November 2017
  PriSC Workshop takes place: 13 January 2018


==
Scope of the Workshop
==

Anyone interested in presenting at the workshop should submit an
extended abstract (up to 2 pages, details below). This can cover past,
ongoing, or future work. Any topic that could be of interest to the
emerging secure compilation community is in scope. Talks that provide
a useful outside view or challenge the community are also welcome.

Topics of interest include but are **not** limited to:

- attacker models for secure compiler chains

- secure compilation properties: full abstraction, memory safety,
control-flow integrity, preserving non-interference or
(hyper-)properties against adversarial contexts,
secure multi-language interoperability

- enforcement mechanisms: static checking, program verification,
reference monitoring, program rewriting, software fault isolation,
system-level protection, secure hardware, crypto, randomization

- experimental evaluation and applications of secure compilation

- proof methods: (bi)simulation, logical relations, game semantics,
multi-language semantics, embedded interpreters

- formal verification of secure compilation chain (protection
mechanisms, compilers, linkers, loaders), machine-checked proofs,
translation validation, property-based testing


==
Guidelines for Submitting Extended Abstracts
==

Extended abstracts should be submitted in PDF format and not exceed 2
pages. They should be formatted in two-column layout, 10pt font, and
be printable on A4 and US Letter sized paper. We recommend using the
new `acmart` LaTeX style in `sigplan` mode:
http://www.sigplan.org/sites/default/files/acmart/current/acmart-sigplanproc.zip

Submissions are not anonymous and should provide sufficient detail to
be assessed by the program committee. Presentation at the workshop
does not preclude publication elsewhere.

Please submit your extended abstracts at https://prisc18.hotcrp.com/


==
Short Talks Session
==

We will also run a short talks session, where participants get five
minutes to present intriguing ideas, advertise ongoing work, etc. You
can expect a call for short talks closer to the event.


==
Program Committee
==

Program Chair
  Catalin Hritcu   Inria Paris

Members
  Amal Ahmed   Inria Paris

[TYPES/announce] Final call for Secure Compilation presentations (PriSC Workshop @ POPL'18)

[Catalin Hritcu]

==

Program Chair
  Catalin Hritcu   Inria Paris

Members
  Amal Ahmed   Inria Paris and Northeastern University
  Lars BirkedalAarhus University
  Dominique Devriese   KU Leuven
  Cédric Fournet   Microsoft Research
  Deepak Garg  MPI-SWS
  Xavier Leroy Inria Paris
  David NaumannStevens Institute of Technology
  Marco Patrignani MPI-SWS
  Frank Piessens   KU Leuven
  Tamara Rezk  Inria Sophia Antipolis
  Nikhil Swamy Microsoft Research


==
Organizing Committee
==

  Amal Ahmed   Inria Paris and Northeastern University
  Dominique Devriese   KU Leuven
  Deepak Garg  MPI-SWS
  Catalin Hritcu   Inria Paris
  Marco Patrignani MPI-SWS
  Tamara Rezk  Inria Sophia Antipolis


==
Contact and More Information
=

More information about PriSC 2018 can be found on the website:
http://popl18.sigplan.org/track/prisc-2018

For questions please contact Catalin Hritcu (Program Chair).

To make sure you receive such announcements in the future please
subscribe to the following low-traffic mailing list:
https://lists.gforge.inria.fr/mailman/listinfo/prisc-announce

[TYPES/announce] Call for Presentations on Secure Compilation (PriSC Workshop @ POPL'18)

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

===
Call for Presentations on Secure Compilation (PriSC Workshop @ POPL'18)
===

Secure compilation is an emerging field that puts together advances in
programming languages, security, verification, systems, compilers, and
hardware architectures in order to devise secure compiler chains that
eliminate many of today's low-level vulnerabilities. Secure
compilation aims to protect high-level language abstractions in
compiled code, even against adversarial low-level contexts, and to
allow sound reasoning about security in the source language. The
emerging secure compilation community aims to achieve this by:
identifying and formalizing properties that secure compilers must
possess; devising efficient enforcement mechanisms; and developing
effective verification and proof techniques.


==
2nd Workshop on Principles of Secure Compilation (PriSC 2018)
==

The Workshop on Principles of Secure Compilation (PriSC) is a new
informal 1-day workshop without any proceedings. The goal is to
identify interesting research directions and open challenges and to
bring together researchers interested in secure compilation.

The 2nd PriSC edition will be held on Saturday, 13 January 2018, in
Los Angeles, together with the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL).

More information at http://popl18.sigplan.org/track/prisc-2018


==
Important Dates
==

  Presentation proposal submission deadline:  18 October 2017, AoE
  Presentation proposal notification: 8 November 2017
  PriSC Workshop takes place: 13 January 2018


==
Scope of the Workshop
==

Anyone interested in presenting at the workshop should submit an
extended abstract (up to 2 pages, details below). This can cover past,
ongoing, or future work. Any topic that could be of interest to the
emerging secure compilation community is in scope. Talks that provide
a useful outside view or challenge the community are also welcome.

Topics of interest include but are **not** limited to:

- attacker models for secure compiler chains

- secure compilation properties: full abstraction, memory safety,
control-flow integrity, preserving non-interference or
(hyper-)properties against adversarial contexts,
secure multi-language interoperability

- enforcement mechanisms: static checking, program verification,
reference monitoring, program rewriting, software fault isolation,
system-level protection, secure hardware, crypto, randomization

- experimental evaluation and applications of secure compilation

- proof methods: (bi)simulation, logical relations, game semantics,
multi-language semantics, embedded interpreters

- formal verification of secure compilation chain (protection
mechanisms, compilers, linkers, loaders), machine-checked proofs,
translation validation, property-based testing


==
Guidelines for Submitting Extended Abstracts
==

Extended abstracts should be submitted in PDF format and not exceed 2
pages. They should be formatted in two-column layout, 10pt font, and
be printable on A4 and US Letter sized paper. We recommend using the
new `acmart` LaTeX style in `sigplan` mode:
http://www.sigplan.org/sites/default/files/acmart/current/acmart-sigplanproc.zip

Submissions are not anonymous and should provide sufficient detail to
be assessed by the program committee. Presentation at the workshop
does not preclude publication elsewhere.

Please submit your extended abstracts at https://prisc18.hotcrp.com/


==
Short Talks Session
==

We will also run a short talks session, where participants get five
minutes to present intriguing ideas, advertise ongoing work, etc. You
can expect a call for short talks closer to the event.


==
Program Committee
==

Program Chair
  Catalin Hritcu   Inria Paris

Members
  Amal Ahmed   Inria Paris and Northeastern University
  Lars BirkedalAarhus University
  Dominique Devriese   KU Leuven
  Cédric

[TYPES/announce] Open positions on secure compilation at Inria Paris funded by ERC grant

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

SECOMP  is a research project aimed
at building the first efficient formally secure compilers for realistic
programming languages. The project brings together a core team at Inria
Paris  lead by Cătălin Hriţcu
 and external
collaborators at University of Pennsylvania
, Portland
State University , MIT
, Northeastern University 
, Microsoft Research , and Draper Labs
. The core team at Inria Paris
 is generously funded for 5 years
(roughly between 2017 and 2021) by a recently awarded ERC Starting Grant
.

Over the duration of the project we are looking for excellent students and
young researchers for Research Internship
, PhD Student
, PostDoc
, Starting Researcher
, and Research Engineer
 positions at Inria Paris
. We can additionally support
exceptional candidates for permanent Researcher
 positions funded and awarded
competitively by Inria. More details about each of these positions are
available
online . Finally, we also have
funding for sabbaticals and short-term visits to Paris for researchers with
an interest in secure compilation.

Regards,
Catalin

[TYPES/announce] Positions for students and young researchers at Inria Paris in Prosecco team

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Prosecco research team  at Inria Paris
 is looking for
excellent, highly motivated students and young researchers for research
internships and PhD, PostDoc, Research Engineer, or Researcher positions.
We have external funding for a couple of PhD and PostDoc positions we can
fill over several years with significant flexibility and can also support
strong candidates for Researcher positions funded and awarded competitively
by Inria.

Prosecco does formal and practical security research on cryptographic
protocols, web security, and hardware security mechanisms. To this end, we
design and implement programming languages, formal verification tools,
dynamic monitors, testing frameworks, verified compilers, etc. Our current
projects include:

   -

   F*: From Program Verification System to Proof Assistant
   (hot topics
   
;
   website ; tutorial
   ; recent paper
   ; code
   )
   -

   miTLS*: Attacking and Proving TLS 1.3 Implementations
   (website ; code ; papers
   ; sample internship topic
   
   )
   -

   Efficient Formally Secure Compilers to a Tagged Architecture
   (brief project description
   
,
   draft paper #1 , paper #2
   
,
   paper #3 , code
   )
   -

   A Verified Browser Security Engine
   (web security models ; defensive
   JavaScript ; sample internship topic
   

   )
   -

   Dependable Property-Based Testing
   (project description
   
,
   paper #1 , paper #2
   , draft paper #3
   , code
   )

PostDocs (usually on 2 year positions) can also propose and follow their
own research agenda and be fairly independent. Researchers (on 3 year

or permanent positions

via a competitive Inria national contest) are expected to be highly
independent. The research internships are for students at any level (BSc,
MSc, and PhD) and usually take between 3 and 6 months. The predominant
language of communication in Prosecco is English.

If you are interested in applying or have any questions please send us an
email at karthikeyan.bharga...@inria.fr and catalin.hri...@gmail.com.

Happy holidays, Karthik and Catalin

[TYPES/announce] The Joint EasyCrypt-F*-CryptoVerif School 2014 in Paris

[Catalin Hritcu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

*** The Joint EasyCrypt-F*-CryptoVerif School ***

Dates: 24-28 November 2014
Place: INRIA office in Paris (23 Avenue d'Italie)
Registration deadline: 1 September
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014

The school is aimed at teaching participants how to use three
state of the art security verification tools: EasyCrypt, F*, and
CryptoVerif, as well as give participants a glimpse of the
beautiful formal foundations behind these tools.

Participants will attend lectures and hands-on tutorials, under
the guidance of members from the tools' developer teams:
- EasyCrypt: Gilles Barthe, François Dupressoir, Benjamin Grégoire,
Benedikt Schmidt, Pierre-Yves Strub
- F*: Karthik Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet,
Cătălin Hriţcu, Chantal Keller, Alfredo Pironti, Pierre-Yves Strub
- CryptoVerif: Bruno Blanchet

There are no registration fees for participants, and we try to
offer grants covering the travel and/or accommodation costs of
the participants who need it. Registration open until 1 September:
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014

EasyCrypt (https://www.easycrypt.info) is a toolset for reasoning
about relational properties of probabilistic computations with
adversarial code. Its main application is the construction and
verification of game-based cryptographic proofs. EasyCrypt was used to
prove the security of complex cryptographic constructions, including
the Cramer-Shoup encryption scheme, the Merkle-Damgaard iterative hash
function design, and the ZAEP encryption scheme. More recently, it has
been used for proving the security of protocols based on garbled
circuits, and for the proof of security for authenticated key-exchange
protocols and derived proofs under weaker assumptions.

F* (https://research.microsoft.com/en-us/projects/fstar/) is a new
ML-like functional programming language designed with program
verification in mind. It has a powerful refinement type-checker that
discharges verification conditions using the Z3 SMT solver. F* has
been successfully used to verify nearly 50,000 lines of code, ranging
from cryptographic protocol implementations to web browser extensions,
and from cloud-hosted web applications to key parts of the F* compiler
itself. The newest version on F* erases to both F# and OCaml, on which
it is based. It also compiles securely to JavaScript, enabling safe
interoperability with arbitrary, untrusted JavaScript libraries.

CryptoVerif (http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/)
is an automatic protocol prover sound in the computational model. It
can prove secrecy and correspondences (e.g. authentication). The
generated proofs are by sequences of games, as used by cryptographers.
CryptoVerif was successfully used for security proofs of FDH
signatures, Kerberos, OEKE, and the SSH transport layer protocol.

More details at:
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014