Postdoc & Scientific Programmer Positions in Tokyo

[Ichiro Hasuo <i.hasuo-HInyCGIudOg@public.gmane.org>]

[-- Attachment #1: Type: text/plain, Size: 108 bytes --]

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


[-- Attachment #2.1: Type: text/plain, Size: 4916 bytes --]

[Please distribute, apologies for multiple postings.]

Open Postdoc & Scientific Programmer Positions in Tokyo

Hasuo Laboratory <https://urldefense.com/v3/__https://group-mmm.org/eratommsd__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F8zLkjWC9$  > at the National
Institute of Informatics <https://urldefense.com/v3/__https://www.nii.ac.jp/en/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F81b76IYh$  >, 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://urldefense.com/v3/__https://group-mmm.org/eratommsd/call-for-students-ja/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F89a4ZHvj$  

Thanks a lot for your consideration.
Best, Ichiro


----
Position 1:
PostDoc Researcher, Category Theory and Practical Model Checking Algorithms
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/postdoc-researcher-category-theory-and-practical-model-checking-algorithms-oct-2022/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F87q9uph3$  

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://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-031-13185-1_12__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F8793XR6J$  
   - Komorida et al., LICS'21
   https://urldefense.com/v3/__https://arxiv.org/abs/2105.10164__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F80a4wpFf$  



----
Position 2:
PostDoc Researcher, Theorem Proving for Automated Driving
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/postdoc-researcher-theorem-proving-for-automated-driving-oct-2022/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F8-XvAwjS$  

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://urldefense.com/v3/__https://arxiv.org/abs/2207.02387__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F82tBPpkZ$  



----
Position 3:
Scientific Programmer towards a Research-Oriented Startup
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/open-position-for-a-scientific-programmer-towards-a-research-oriented-startup/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F81AQ0dzW$  

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-HInyCGIudOg@public.gmane.org     Secretaries: hasuolab-secr-5aC7G4kDdWR4Eiagz67IpQ@public.gmane.org
https://urldefense.com/v3/__http://group-mmm.org/*ichiro/__;fg!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F86jT7V9U$  

[-- Attachment #2.2: Type: text/html, Size: 6402 bytes --]