[TYPES/announce] Highlights of Logic, Games, and Automata 2021: 3rd Call for Presentations

[Sławomir Lasota]

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



HIGHLIGHTS 2021: 9th annual conference on Highlights of LOGIC, GAMES, and
AUTOMATA

15-17 September 2021, online (originally planned to be held in Aachen)
http://highlights-conference.org

We invite submissions for contributed talks (around 10 minutes).

IMPORTANT DATES:
+ Submission deadline: 4 JUNE AoE
+ Notification:   18 JUNE

SUBMISSION WEB PAGE: https://easychair.org/conferences/?conf=highlights2021



HIGHLIGHTS 2021 is the 9th conference on Highlights of Logic, Games, and
Automata that aims to integrate the diverse research community working in
the areas of Logic, Finite Model Theory, Automata Theory, Games and
Verification. Individual papers are dispersed across many conferences,
which makes them challenging to follow. Participating in the annual
Highlights conference offers a wide picture of the latest research in the
field and a chance to meet and interact with most of the members of the
research community. The speakers are encouraged to present their best
recent work at Highlights, whether already published elsewhere or not.

The three-day conference (15-17 September) will be preceded by a tutorial
day
(14 September). This year's edition will be held online, with no
registration fees
or with a moderate one (around 10 EUR).

TUTORIALS (September 14)
+ Christoph Haase,  "A guided tour through Presburger arithmetic and
friends"
+ Michał Pilipczuk, "Old and new advances in model checking first order
logic"

KEYNOTES
+ Rajeev Alur
+ Balder ten Cate
+ Karoliina Lehtinen
+ Nutan Limaye
+ Joel Ouaknine

[TYPES/announce] ML Family Workshop 2021: deadline extension

[Jonathan Protzenko]

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

The deadline for the ML family workshop has been extended by a week. If 
you were on the fence, please submit!


---

We are happy to announce that the ML Family Workshop is back for its 
2021 edition, which we will be held online on Thursday August 26th, in 
conjunction with ICFP 2021.


The ML family workshop warmly welcomes submission touching on the 
programming languages traditionally seen as part of the "ML family" 
(Standard ML, OCaml, F#, CakeML, SML#, Manticore, MetaOCaml, etc.). The 
scope of the workshop includes all aspects of the design, semantics, 
theory, application, implementation, and teaching of the members of the 
ML family. We also encourage presentations from related languages (such 
as Haskell, Scala, Rust, Nemerle, Links, Koka, F*, Eff, ATS, etc), to 
exchange experience of further developing ML ideas.


## Submission details

Submissions must be at most three pages long; see the full call for 
papers 
 
for details.


Submission site: https://ml21.hotcrp.com/

## Important dates

Thu, Jun 3th 2021 (AoE): submission deadline
Thu, Jun 24th 2021 (AoE): author notification
Thu, Aug 26th: workshop (time slots TBD)

## Program committee

Danel Ahman (University of Ljubljana)
Robert Atkey (University of Strathclyde)
Frédéric Bour (Tarides)
Ezgi Çiçek (Facebook London)
Youyou Cong (Tokyo Institute of Technology)
Richard A. Eisenberg (Tweag I/O)
Martin Elsman (University of Copenhagen, Denmark)
Ohad Kammar (University of Edinburgh)
Naoki Kobayashi (University of Tokyo, Japan)
Benoît Montagu (Inria)
Jonathan Protzenko (Microsoft Research) (Chair)
Kristina Sojakova (INRIA Paris)
Don Syme (Microsoft)
Matías Toro (University of Chile)
Katsuhiro Ueno (Tohoku University)

[TYPES/announce] PhD position on the formalization of logical calculi in Saarbrücken

[Andrei Popescu]

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

A PhD position is open at the MPI for Informatics in Saarbrücken,
supervised by Christoph Weidenbach, Jasmin Blanchette and Sophie
Tourret. The project is about using Isabelle/HOL to formalize logical
calculi.

See https://www.cs.vu.nl/~jbe248/sb_job.html for more information.

[TYPES/announce] PhD student and post-doc positions in Program Verification at ETH Zurich

[Mueller Peter]

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

The Programming Methodology group (http://www.pm.inf.ethz.ch/) at ETH Zurich is 
recruiting PhD students and post-docs in the area of program verification. We 
are especially interested in strengthening our teams working on Rust 
verification (https://www.pm.inf.ethz.ch/research/prusti.html) and Go 
verification (https://www.pm.inf.ethz.ch/research/gobra.html). Our goal is to 
develop verification techniques and tools that can be used to prove correctness 
and security of advanced systems.
Key requirements for successful applications:
* Strong commitment to research
* Interest in combining theory and practice
* For PhD students: excellent M.Sc. degree in Computer Science or in a related 
subject with a strong Computer Science component
* For post-docs: publications in top conferences or journals
* Proficiency in English and excellent communication skills, both oral and 
written
Applications and questions should be sent to Peter Müller 
(jobs...@inf.ethz.ch). The application should 
include a CV and a description of research interests. We will consider 
applications until the positions are filled. The start date is negotiable.
More details about the positions:
* PhD and post-doc positions are fully funded and have an attractive salary and 
social benefits.
* Full scholarships are available for outstanding B.Sc. students interested in 
the PhD.
* ETH has one of the top computer science departments in the world
* Zurich is consistently ranked among the top destinations in the world for 
quality of life.
General information on doctoral studies at ETH is available at 
www.inf.ethz.ch/doctorate.html

[TYPES/announce] PhD position on program verification in Coq

[David Nowak]

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


Dear all,

We have an opening for a 3-year PhD position at University of Lille,
France. The successful applicant will be funded -- including salary
and (international) conference travel -- through a new French-German
ANR-funded project. There will also be an opportunity to collaborate
with a research team in Japan.

Lille is at the heart of Europe: 45 minutes from Bruxelles, 1 hour
from Paris, 1 hour and half from London. This is an important
university hub that hosts the annual International Cybersecurity Forum
(FIC).

The start date is September 1st, but might possibly be postponed to
October 1st.

The PhD position is about the formal proof in Coq for shallow-embedded
imperative programs and their compilation into C (more details below).

Interested students should meet the following requirements:

- Be interested by the topic of the PhD :-)

- Have or be about to complete a Master in Computer Science or a
  related field (Logic, Mathematics, etc.).

If you are interested in applying for this opportunity please begin by
contacting us {gilles.grimaud,samuel.hym,david.nowak}@univ-lille.fr 

as soon as possible with the following information:

- CV/Resume

- A brief introduction of yourself, your scientific interests, and if
  you are familiar with any of the following topics:
  * formal proof / formal verification,
  * functional programming
  * monads
  * semantics

———
Summary:

The topic of this PhD offer is the formal proof in Coq for
shallow-embedded imperative programs and their compilation into C.
More precisely, the objective is to conceive and develop formal tools
to simplify code writing and proof of system software for low-end
devices.

Context:

The Coq proof assistant [1] allows to prove properties of programs.
Its language, called Gallina, is purely functional. In the Pip project [2],
we have considered a monadic subset of C-like Gallina enough to
formally write an OS kernel.

Objectives:

A first objective of this PhD is to extend the monadic subset in order
to include further imperative features (such as loops, references or
exceptions) that will simplify code writing and proof of system
software for low-end devices. For security properties the monadic
Hoare logic used for Pip will have to be extended to deal with the new
imperative features. For functional properties, there are two possible
directions: either use the monadic Hoare logic or monadic equational
reasoning as developed in Monae [3]. The relation with FreeSpec [4]
should also be investigated.

A second objective is to automatically translate programs written in
this monadic subset into an AST of the CompCert C verified compiler
[5] and to prove formally that this translation is correct, in the
sense that properties proved on the monadic subset are also true of
the generated C code.

[1] https://coq.inria.fr 
[2] http://pip.univ-lille1.fr 
[3] https://github.com/affeldt-aist/monae 

[4] https://github.com/lthms/FreeSpec 
[5] https://compcert.org 
———

All the best,

-- 
Gilles Grimaud, Samuel Hym, David Nowak