The Coq mailing list

[Ichiro Hasuo <i.hasuo AT acm.org>]

[Please distribute, apologies for multiple postings.]

Open Postdoc & Scientific Programmer Positions in Tokyo

Hasuo Laboratory at the National Institute of Informatics, Tokyo, Japan invites applications for a scientific programmer and a postdoc researcher. The positions are funded by a JST ERATO project (scientific research) and a JST START project (practical development towards a research-oriented startup), and their scopes are largely the application of foundational research on logic and semantics to real-world problems. See below for the specific scope of each position. The positions are for ~2.5 years max.

We are also constantly looking for PhD students. https://group-mmm.org/eratommsd/call-for-students-ja/

Thanks a lot for your consideration.

Best, Ichiro

---- 

Position 1: 

PostDoc Researcher, Category Theory and Practical Model Checking Algorithms

https://group-mmm.org/eratommsd/postdoc-researcher-category-theory-and-practical-model-checking-algorithms-oct-2022/

We aim to push the landscape of categorical studies (especially on coalgebras) to the modeling of state-of-the-art practical algorithms for formal verification (model checking, game solving, system abstraction, etc.). The position will be especially suited for researchers with coalgebraic and related backgrounds who want to see their results in action as practical verification algorithms.

Key publications: 

• Kori et al., CAV'22
  https://link.springer.com/chapter/10.1007/978-3-031-13185-1_12
  
• Komorida et al., LICS'21
  https://arxiv.org/abs/2105.10164
  

---- 

Position 2: 

PostDoc Researcher, Theorem Proving for Automated Driving

https://group-mmm.org/eratommsd/postdoc-researcher-theorem-proving-for-automated-driving-oct-2022/

We aim to develop a comprehensive set of techniques for proving the safety of automated driving. Its core consists of a custom-made program logic and its proof checker; however, elements outside conventional theorem proving studies will be pursued, too, such as heuristics for proof discoveries, implementation of safety proofs in automated driving cars, studying the roles of safety proofs in explainability and social acceptance of automated driving, etc. The position is highly recommended for theorem proving researchers who wish to apply their expertise to a hot application domain (namely automated driving), and furthermore, obtain novel theoretical insights in return from the real-world application. The commercialization of the research output is also planned, with the founding of a spin-off startup (cf. our call for a scientific programmer below).

Key publication: 

• Hasuo et al., IEEE Trans. Intelligent Vehicles, to appear. https://arxiv.org/abs/2207.02387

---- 

Position 3: 

Scientific Programmer towards a Research-Oriented Startup

https://group-mmm.org/eratommsd/open-position-for-a-scientific-programmer-towards-a-research-oriented-startup/

A programmer position under government research funding towards a research-oriented startup. An excellent opportunity for those who value both the scientific pursuit of novelties and industrial and social impacts. We look for programmers with a formal logic background. Come join us on the venture!

======
Ichiro Hasuo
Professor, National Institute of Informatics
i.hasuo AT acm.org     Secretaries: hasuolab-secr AT nii.ac.jp
http://group-mmm.org/~ichiro/