[TYPES/announce] 28th WoLLIC 2022 - First Call for Papers

[Ruy Jose Guerra Barretto de Queiroz]

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

[Please distribute. Apologies for multiple postings]

CALL FOR PAPERS

WoLLIC 2022
28th Workshop on Logic, Language, Information and Computation
September 20 to 23, 2022
Iași, Romania

ORGANISATION
Faculty of Computer Science, Alexandru Ioan Cuza University, Romania
Centro de Informática, Universidade Federal de Pernambuco, Brazil

CALL FOR PAPERS
WoLLIC is an annual international forum on inter-disciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning. Each meeting includes invited talks and tutorials
as well as contributed papers. The twenty-eighth WoLLIC will be held at the
Faculty of Computer Science, Alexandru Ioan Cuza University, Iași, Romania,
September 20 to 23, 2022.  It is scientifically sponsored by the
Association for Symbolic Logic (ASL), the Interest Group in Pure and
Applied Logics (IGPL), the The Association for Logic, Language and
Information (FoLLI), the European Association for Theoretical Computer
Science (EATCS) (tbc), and the Sociedade Brasileira de Lógica (SBL).

ABOUT THE LOCATION
Iași 
https://urldefense.com/v3/__https://www.uaic.ro/en/iasi-2/__;!!IBzWLUs!CAFHPJ4OsfRI4PeatmrB_3l3RB5urET0fPIYJwxioMAhMjRnse7neOa3jU8YdbJrms4beLXhKsY3cQ$
 

PAPER SUBMISSION
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are: foundations of computing, programming and Artificial
Intelligence (AI); novel computation models and paradigms; broad notions of
proof and belief; proof mining, type theory, effective learnability and
explainable AI; formal methods in software and hardware development;
logical approach to natural language and reasoning; logics of programs,
actions and resources; foundational aspects of information organization,
search, flow, sharing, and protection; foundations of mathematics;
philosophical logic; philosophy of language.
Proposed contributions should be in English, and consist of a scholarly
exposition accessible to the non-specialist, including motivation,
background, and comparison with related works. Articles should be written
in the LaTeX format of LNCS by Springer (see author's instructions at
https://urldefense.com/v3/__http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0__;!!IBzWLUs!CAFHPJ4OsfRI4PeatmrB_3l3RB5urET0fPIYJwxioMAhMjRnse7neOa3jU8YdbJrms4beLUjjWnquw$
 ). They must
not exceed 12 pages, with up to 5 additional pages for references and
technical appendices. The paper's main results must not be published or
submitted for publication in refereed venues, including journals and other
scientific meetings.
It is expected that each accepted paper be presented at the meeting by one
of its authors. (At least one author is required to pay the registration
fee before granting that the paper will be published in the proceedings.)
Papers must be submitted electronically at the WoLLIC 2022 EasyChair
website 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=wollic2022__;!!IBzWLUs!CAFHPJ4OsfRI4PeatmrB_3l3RB5urET0fPIYJwxioMAhMjRnse7neOa3jU8YdbJrms4beLV23WQVAA$
 .

PROCEEDINGS
The proceedings of WoLLIC 2022, including both invited and contributed
papers, will be published in advance of the meeting as a volume in
Springer's LNCS series. In addition, abstracts will be published in the
Conference Report section of the Logic Journal of the IGPL, and selected
contributions will be published (after a new round of reviewing) as a
special post-conference WoLLIC 2022 issue of a scientific journal (to be
confirmed).

INVITED SPEAKERS
(tba)

IMPORTANT DATES
April 30, 2022: Abstract deadline
May 7, 2022: Full paper deadline
June 15, 2022: Author notification
June 26, 2022: Final version deadline (firm)

PROGRAMME COMMITTEE
Agata Ciabattoni (Technische Universität Wien) (Co-Chair)
Diana Costa (University of Lisbon)
Hans van Ditmarsch (Open University of the Netherlands)
Roman Kuznets (Technische Universität Wien)
João Marcos (Univ Federal do Rio Grande do Norte)
Larry Moss (Indiana University Bloomington)
Valeria de Paiva (Topos Institute and PUC-Rio)
Elaine Pimentel (Univ Federal do Rio Grande do Norte) (Co-Chair)
Revantha Ramanayake (University of Groningen)
Mehrnoosh Sadrzadeh (University College London)
Alexandra Silva (Cornell University)
Alex Simpson (University of Ljubljana)
Sonja Smets (University of Amsterdam)
Alwen Tiu (The Australian National University)
Leon van der Torre (University of Luxembourg)
Andrea Aler Tubella (Umeå University)
Andres Villaveces (Universidad Nacional de Colombia)
Renata Wassermann (Universidade de São Paulo)
(MORE TBC)

STEERING COMMITTEE
Samson Abramsky, Anuj Dawar, Juliette Kennedy, Ulrich Kohlenbach, Daniel
Leivant, Leonid Libkin, Lawrence Moss, Luke Ong, Valeria de Paiva, Ruy de
Queiroz, Alexandra Silva, Renata Wassermann.

ADVISORY COMMITTEE
Johan van Benthem, 

[TYPES/announce] FORMATS 2022: first call for papers

[Gethin Norman]

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

FORMATS 2022: FIRST CALL FOR PAPERS

20th International Conference on Formal Modeling and Analysis of Timed Systems

https://urldefense.com/v3/__https://conferences.ncl.ac.uk/formats2022/__;!!IBzWLUs!BOHDApCNnQCOFEiQZ7lgTzcsyd6Ga9ps_1WJzpfji_AcrOivq0VZ-TKJIgc7Yim4EW5Im6bW4GMx6Q$
 

12-17 September 2022, Warsaw, Poland
co-located with CONCUR, FMICS and QEST as part of CONFEST 2022

SCOPE & TOPICS

FORMATS (International Conference on Formal Modeling and Analysis of Timed 
Systems) is an annual conference which aims to promote the study of fundamental 
and practical aspects of timed systems, and to bring together researchers from 
different disciplines that share interests in the modelling, design and 
analysis of timed computational systems. The conference aims to attract 
researchers interested in real-time issues in hardware design, performance 
analysis, real-time software, scheduling, semantics and verification of 
real-timed, hybrid and probabilistic systems.

Typical topics include (but are not limited to):

 • Foundations and Semantics: Theoretical foundations of timed systems, 
languages and models (e.g., timed automata, timed Petri nets, hybrid automata, 
timed process algebra, max-plus algebra, probabilistic models).

 • Methods and Tools: Techniques, algorithms, data structures, and software 
tools for analyzing timed systems and resolving temporal constraints (e.g., 
scheduling, worst-case execution time analysis,optimization, model checking, 
testing, constraint solving).

 • Applications: Adaptation and specialization of timing technology in 
application domains in which timing plays an important role (e.g., real-time 
software, hardware circuits, scheduling in manufacturing and telecommunication, 
robotics).

New for this year, FORMATS will incorporate a special track on:

 • Learning-based and data-driven systems: We particularly encourage papers 
that exploit synergies between the formal analysis of timed systems and 
data-driven techniques (such as reinforcement learning or deep learning), or 
which target application domains where learning is important (such as robotics 
or autonomous systems).

PAPER SUBMISSION

FORMATS 2022 solicits high-quality papers reporting research results, 
experience reports and/or tools related to the topics mentioned above. 
Submitted papers must contain original, unpublished contributions, not 
submitted for publication elsewhere. The papers should be submitted 
electronically in PDF, following the Springer LNCS style guidelines. Two 
categories of papers are invited:

 • Regular papers, which should not exceed 15 pages in length
 • Short papers, which should not exceed 7 pages in length

Both page limits exclude references, which are not limited in length. If 
necessary, the paper may be supplemented with a clearly marked appendix, which 
will be reviewed at the discretion of the program committee. Each paper will 
undergo a thorough review process. Papers should be submitted electronically 
via the EasyChair online submission system: 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=formats2022__;!!IBzWLUs!BOHDApCNnQCOFEiQZ7lgTzcsyd6Ga9ps_1WJzpfji_AcrOivq0VZ-TKJIgc7Yim4EW5Im6btbrXVaQ$
  

ARTIFACT EVALUATION

This year, FORMATS is encouraging authors to submit artifacts where 
appropriate, for example to demonstrate how to reproduce experimental data in a 
research paper or to examine the usability and applicability of a software 
tool. Artifacts will be submitted and evaluated only for papers accepted for 
publication. These will be evaluated by the Artifact Evaluation Committee and 
those that are accepted will receive a repeatability badge to be displayed on 
the first page of the published version.

PUBLICATION AND BEST PAPER AWARD

The proceedings of FORMATS 2022 will be published by Springer in the Lecture 
Notes in Computer Science series. The best paper of the conference will be 
awarded the Oded Maler Award in Timed Systems.

IMPORTANT DATES

 • Abstract submission: 19 April 2022
 • Paper submission: 22 April 2022
 • Acceptance notification: 17 June 2022
 • Artifact submission deadline: 24 June 2022
 • Camera-ready copy deadline: 15 July 2022
 • Conference: 12-17 September 2022

CONFEST 2022, which includes FORMATS 2022, is currently planned as a physical, 
in-person event with support for remote presence for speakers and participants. 
Depending on the pandemic situation, a decision whether to cancel the physical 
component of CONFEST or not will be made by the end of June 2022.

​​For any questions, feel free to contact the program chairs Sergiy Bogomolov 
(sergiy.bogomo...@ncl.ac.uk) and David Parker (d.a.par...@cs.bham.ac.uk).

ORGANISATION

Program Chairs
• Sergiy Bogomolov (UK)
• David Parker (UK)

Artifact Evaluation Chairs
• Akshay Rajhans (USA)
• Paolo Zuliani (UK)

Publicity Chair
• Gethin Norman (UK)

Special 

[TYPES/announce] Rust Verification Workshop at ETAPS 2022: Call for Talk and Demo Proposals

[Mueller Peter]

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

Call for Talk, Demo, and Challenge Proposals
2nd Rust Verification Workshop
Co-located with ETAPS 2022
Munich
Sunday, April 03, 2022
https://urldefense.com/v3/__https://sites.google.com/view/rustverify2022/home__;!!IBzWLUs!G4xwjmn6v93mHpZ6Tt37BnYL14gdxWDDKZgSwlO-9Sfrs9hqogM9RNBGcF9FAYII5X9yrr7wYQZqUg$
 

Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.
The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.
We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.

Call for Talk and Demo Proposals
-
We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.
We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.
Please submit by email to 
peter.muel...@inf.ethz.ch.

Important Dates
-
Deadline for talk/demo proposals:January 14, 2022 (Friday)
Notification of acceptance: February 07, 2022 (Monday)
Workshop:   April 03, 2022 (Sunday)

Organizers

Rajeev Joshi, Amazon Web Services 
mailto:joraj...@amazon.com>>
Nicholas Matsakis, Mozilla mailto:nmatsa...@mozilla.com>>
Peter Müller, ETH Zurich 

[TYPES/announce] Postdoc Position on Verification of Concurrent Systems via Model Learning, Royal Holloway University of London -- Application deadline 9 Jan 2022

[Matteo Sammartino]

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

- Application deadline: Midnight, 9 Jan 2022
- Starting date: As soon as possible
- Salary: £35,931-£37,979
- Duration: until February 2023


Applications are invited for the post of Post-Doctoral Research Assistant in 
the Computer Science Department at Royal Holloway, University of London.

Successful applicants will be working on the EPSRC-funded "Verification of 
Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led 
by Alexandra Silva (UCL/Cornell) and Matteo Sammartino (Royal Holloway 
University of London).

This is a joint research effort involving Royal Holloway University of London, 
University College London, and ARM, world-leading designer of multi-core chips.

For an informal discussion about the post, please contact Dr. Matteo Sammartino 
on matteo.sammart...@rhul.ac.uk.


# Project Description

Digital devices increasingly rely on multi-threaded computation, with 
sophisticated concurrent behaviour becoming prevalent at any scale. As the 
complexity of these systems increases, there is a pressing need to automate the 
assessment of their correctness, especially with respect to concurrency-related 
aspects. Formal verification provides highly effective techniques to assess the 
correctness of systems. However, formal models are usually built by humans, and 
as such can be error-prone and inaccurate.

The CLeVer project aims to:

- develop a novel verification framework that relies on learning techniques to 
automatically build and verify models of concurrency, with a particular focus 
on multi-core systems.

- apply the framework to real-world verification tasks, in collaboration with 
ARM.

# The ideal candidate

We are looking for candidates with a PhD in one of the following areas: 
model-based testing and verification, formal methods for concurrency, automated 
analysis of hardware systems. Experience in multiple areas will be valued. 
Candidates ideally should also have strong programming skills.

# Where to apply

https://urldefense.com/v3/__https://jobs.royalholloway.ac.uk/0721-259-R-R__;!!IBzWLUs!GBUI4ogBjKihbUy7Zjvs5uy-jYLfnkDBmHoLxe66Aocp0u-vNUn0dwNvEzw0ElB4e1xgKh3NbHDrlQ$
 

[TYPES/announce] 1+2 Assistant positions at Chalmers on ICT and Basic Science

[Ana Bove]

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


Dear All,

Chalmers has now opened 11 tenured Assistant professor positions 
 among them
* *one* in *ICT* area: 
https://urldefense.com/v3/__https://www.chalmers.se/en/about-chalmers/Working-at-Chalmers/Vacancies/Pages/default.aspx?rmpage=job=9987__;!!IBzWLUs!Ed7dp1ZoB0rwnIeO_-3iUF-bR3RRiHeXf4cDQ4yU7np06eS35XHdek4p88WeChrRkol8ap4M7k8HaQ$ 
* *two* in *Basic science*: 
https://urldefense.com/v3/__https://www.chalmers.se/en/about-chalmers/Working-at-Chalmers/Vacancies/Pages/default.aspx?rmpage=job=9989__;!!IBzWLUs!Ed7dp1ZoB0rwnIeO_-3iUF-bR3RRiHeXf4cDQ4yU7np06eS35XHdek4p88WeChrRkol8ap5LuI--pg$ 

The positions comes with a starting package, you can read more about 
this and other conditions in the links above.


We encourage all strong candidates to apply, in particular women and 
other minorities.


Please distribute this information to those you think could fit the profile.

Thanks

--
-- Ana Bove, Docent
email: bove(at)chalmers.se
Phone: (46)(31)7721020
https://urldefense.com/v3/__http://www.cse.chalmers.se/*bove__;fg!!IBzWLUs!Ed7dp1ZoB0rwnIeO_-3iUF-bR3RRiHeXf4cDQ4yU7np06eS35XHdek4p88WeChrRkol8ap6E6nJfbA$ 
Department of Computer Science and Engineering

Chalmers Univ. of Technology and Univ. of Gothenburg

[TYPES/announce] 10 PhD studentships in Nottingham

[Graham Hutton]

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

Dear all,

The School of Computer Science at the University of Nottingham 
in the UK is seeking applications for 10 fully-funded PhD
studentships: 
https://urldefense.com/v3/__https://tinyurl.com/ten-phd-2021__;!!IBzWLUs!FPOJPjJY-7d-34zMA-4YhOgqorzvT_AbWrXzdkPjIAiUkOZ-QohwBW0cNhyD1RPGceGhtUYVWb8WSA$
 

Applicants in the area of the Functional Programming Lab
(tinyurl.com/fp-notts) are strongly encouraged!  If you are
interested in applying, please contact a potential supervisor
as soon as possible; the application deadline is 13th Feb:

  Thorsten Altenkirch - constructive logic, proof assistants,
  homotopy type theory, category theory, lambda calculus.
 
  Graham Hutton - functional programming, haskell, category
  theory, program verification, program calculation.

  Nicolai Kraus - homotopy type theory, higher category theory,
  constructive mathematics, and related topics.

The studentships are open to applicants of any nationality.

Best wishes,

Graham Hutton 

+---+

  10 Fully-Funded PhD Studentships

 School of Computer Science
University of Nottingham, UK

   tinyurl.com/ten-phd-2021

Applications are invited from international and home students
for 10 fully-funded PhD studentships offered by the School of
Computer Science, starting on 1st October 2022.

The topics for the studentships are open, but should relate to
interests of one of the School's research groups: Computational
Optimisation and Learning; Computer Vision; Cyber Security;
Functional Programming; Intelligent Modelling and Analysis;
Mixed Reality; Uncertainty in Data and Decision Making.

The studentships are fully-funded for 3.5 years and include a
stipend of £15,009 per year and tuition fees.  Applicants are
normally expected to have a first class bachelors or masters
degree in Computer Science or another relevant area, and must
obtain the support of a potential supervisor in the School
prior to submitting their application.

If you are interested in applying, please contact a potential
supervisor as soon as possible, and at least two weeks prior
to the closing date.  If the supervisor wishes to support
your application, they will direct you to make an official
application through the MyNottingham system.

Closing date for applications: Sunday 13th February 2022.

+---+




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

[TYPES/announce] SYCO 8 - Final Call for Participation

[Maaike Zwart]

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

  
CALL FOR PARTICIPATION
EIGHTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 8)

In person at Tallinn University of Technology, Estonia
Also online.
13-14 December 2021

Registration deadline: 6 December 2021 (AoE)
Please register even when attending online.

https://urldefense.com/v3/__https://www.cl.cam.ac.uk/events/syco/8/__;!!IBzWLUs!ArC6yKd-bKyeUi1kcUpC3hzY15fYQ2sZFTtyVy8rgf9wF4RSimzNhzMrdvWnME0Jr3HvNlXOq3bg8g$
 


The Symposium on Compositional Structures (SYCO) is an
interdisciplinary series of meetings aiming to support the growing
community of researchers interested in the phenomenon of
compositionality, from both applied and abstract perspectives, and in
particular where category theory serves as a unifying common language.
Previous SYCO events have been held at University of Birmingham,
University of Strathclyde, University of Oxford, Chapman University,
and University of Leicester.

SYCO 8 will be held both at Tallinn University of Technology and online,
replacing the cancelled SYCO 7. The programme consists of
2 invited talks and 16 contributed talks.


INVITED TALKS

* John van de Wetering (Radboud University Nijmegen)
*   - Categorical approaches to reconstructing quantum theory*

* Christine Tasson (Sorbonne Université)
*   - A multicategorical approach to mixed linear-non-linear substitution*


CONTRIBUTED TALKS
Full schedule available at 
https://urldefense.com/v3/__https://www.cl.cam.ac.uk/events/syco/8/__;!!IBzWLUs!ArC6yKd-bKyeUi1kcUpC3hzY15fYQ2sZFTtyVy8rgf9wF4RSimzNhzMrdvWnME0Jr3HvNlXOq3bg8g$
 

* Stefan Zetzsche, Gerco van Heerdt, Matteo Sammartino and Alexandra Silva
   - Canonical automata via distributive law homomorphisms
* Simon Henry and Nicholas Meadows
   - Higher Theories and Monads
* Paulina Goedicke and Jamie Vicary
   - A Category Theoretical Description of Block Designs and Quantum Designs
* Vincent Wang-Mascianica and Bob Coecke
   - Talking Space: Inference from spatial linguistic meanings
* Lukas Heidemann
   - Frames in pretriangulated dg-categories
* Elena Di Lavore, Wilmer Leal and Valeria de Paiva
   - Dialectica Petri nets
* George Kaye, Dan Ghica and David Sprunger
   - Normalisation by evaluation for digital circuits
* Guillaume Boisseau and Robin Piedeleu
   - Graphical Piecewise-Linear Algebra
* Liliane-Joy Dandy, Emmanuel Jeandel and Vladimir Zamdzhiev
   - Qimaera: Type-safe (Variational) Quantum Programming in Idris
* Matt Wilson and Augustin Vanrietvelde
   - Composable constraints
* Davide Trotta, Matteo Spadetto and Valeria de Paiva
   - Dialectica Logical Principles
* Simon Fortier-Garceau
   - Interventions and Counterfactuals for Categorical Models of Causality
* Vikraman Choudhury
   - Weighted sets and modalities
* Elena Di Lavore and Pawel Sobocinski
   - Monoidal width
* Dylan McDermott and Alan Mycroft
   - On the relation between call-by-value and call-by-name
* Olivier Peltre
   - Homological algebra for message-passing algorithms


REGISTRATION

Registration is open until the 6th of December, 2021.
You can register for either the in person meeting or
for the online event.

Please register via:
https://urldefense.com/v3/__https://docs.google.com/forms/d/e/1FAIpQLSfAgcQnimYJPM2msBraTU_0k-8zAqwwalYzpSgVtfKgfjkptA/viewform__;!!IBzWLUs!ArC6yKd-bKyeUi1kcUpC3hzY15fYQ2sZFTtyVy8rgf9wF4RSimzNhzMrdvWnME0Jr3HvNlXG0LtoQw$
 
Registration is free.

More details are available on the conference website:
https://urldefense.com/v3/__https://www.cl.cam.ac.uk/events/syco/8/__;!!IBzWLUs!ArC6yKd-bKyeUi1kcUpC3hzY15fYQ2sZFTtyVy8rgf9wF4RSimzNhzMrdvWnME0Jr3HvNlXOq3bg8g$
 


COVID-19 SITUATION IN ESTONIA

The number of covid cases in Estonia is sharply declining,
so we feel confident to go ahead with SYCO 8.
We are aware of the new Omicron variant, but according to
the WHO there is as yet insufficient data to draw any conclusions
about its effect on the vaccinated population.

We are therefore carrying on with the event in a hybrid form,
as planned. We invite those who are willing,
and have proof of recovery and/or vaccination,
to participate in person.

However, each country is imposing its own new travel restrictions.
So please check your own country's regulations before booking.

At the moment, for the UK, EU, and Schengen countries, proof of
vaccination or recovery, and filling out a passenger locator form,
is sufficient to enter Estonia. You do not need to get tested or
isolate if you fulfill these requirements. Please consult the government
web page for the latest regulations:

[TYPES/announce] Postdoc position in quantum formal verification @ Université Paris-Saclay, CEA List, France

[christophe chareton]

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

The emerging quantum software group @ CEA List, Université Paris-Saclay,
offers
a two years fully-funded postdoctoral position at the crossroad of quantum
programming, program analysis and formal methods.


=== OUR GROUP

We are an emerging group in formal verification and static analysis of
quantum
programs, integrated in the Software Safety Laboratory of CEA List,
Université
Paris-Saclay. Our long term goal is to design and develop formal techniques
and
tools enabling productive and certified quantum programming. Especially, we
develop Qbricks [1], a proof of concept environment for formally verified
quantum programming language.

See our website at 
https://urldefense.com/v3/__https://qbricks.github.io/__;!!IBzWLUs!DTmRMuyfh6ehH9DSFJaqLMIs4YlesQRyI8Q8dkpjvQlB5Tx-NTs4Fg265PDuyMEj-jAvzHF-RqvC7g$
  for additional information.

=== ABOUT THE POSTDOC POSITION

Adapting the best practice for classical computing formal verification --
deductive
verification, first order logic reasoning--, our recent development of
Qbricks enables
formal specification -- circuit well-formedness, functional behavior,
complexity --
and verification for quantum programming with ideal qubits. The goal of
this post-
doctoral position is to extend  this practice to quantum compilation and
physical
qubits implementations.  Possibilities include, among others, error
correction
mechanisms in certified quantum code, together with specifications and
reasoning
technique for certifying its reliability, automatized certified optimizer
for quantum
circuits, hardware agnostic assembly language together
with its compiler, qubit mapping, etc

Keywords: quantum programming, compilation, optimization, formal
verification, deductive
verification


=== HOW TO APPLY

Applications should be sent to christophe.char...@cea.fr as soon as
possible
(first come, first served) and by early February 2021 at the latest.
Candidates
should send a CV, a cover letter, a transcript of all their university
results,
as well as contact information of two references. The  position is expected
to
start in May 2021.

Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA)
Contact: christophe.chare...@cea.fr, sebastien.bar...@cea.fr


[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An
Automated
Deductive Verification Framework for Circuit-building Quantum Programs.
ESOP
2021.