NB: This Call is Already Closed.
NB. There is another researcher call that we are currently advertising. The current call may be closed early if we have a good candidate for this other call.
ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD) invites applications for a postdoc researcher. We aim to push the landscape of categorical studies (especially on coalgebras, described e.g. in the textbook by Jacobs) 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.
JOB DESCRIPTION
The candidate will work at National Institute of Informatics, Tokyo, Japan, and will pursue categorical foundations of state-of-the-art verification algorithms, which will in turn yield generic “categorical programs” for a variety of problems (deterministic and probabilistic, qualitative and quantitative, etc.).
On the one hand, many recent verification algorithms—such as those presented in CAV and TACAS—seem to be built on rich theoretical (categorical and lattice-theoretic) foundations, but these foundations are often yet to be explicated, offering great research opportunities for semantics researchers. On the other hand, thanks to the level of (categorical) abstraction enabled by modern programming languages such as Haskell, a lot of “categorical pseudocode”—the outcome of our categorical studies—can be literally programmed nowadays. Such categorically derived programs can be instantiated to a variety of problems and make real-world impacts. We observed this fruitful two-way relationship between category theory and practical algorithms in our recent paper [Kori, Urabe, Katsumata, Suenaga & Hasuo, CAV’22].
The advertised position will be especially suited for early-career researchers with categorical (coalgebraic and related) backgrounds who want to broaden their research portfolio and apply their categorical results to practical problems. We believe our group in Tokyo is one of the best places to do so, with our proven record of theoretical studies (including LICS’21, CONCUR’21, MFPS’21, MFPS’20, LICS’19) as well as studies of practical verification algorithms (including CAV’22, CAV’21, CAV’20, TACAS’19). We can even draw inspiration from other lines of research of ours, such as model-guided testing heuristics (e.g. FM’21, CAV’19), timed automata (e.g. NFM’22, CAV’19), and safety proofs for automated driving (IEEE T-IV ’22).
The candidate will work closely with Prof. Ichiro Hasuo and a few other team members. It is possible that the candidate be granted an academic title (such as Project Assistant/Associate Professor).
ESSENTIAL SKILLS AND REQUIREMENTS
- Motivated, dedicated, and able to work both independently and collaboratively
- Proven publication record
- Proven expertise in coalgebras, fibrations, fixed-point theory, and predicate transformers, or (proven expertise in at least one plus eagerness to learn the other)
- Familiarity with, or eagerness to learn, formal verification algorithms and their implementation
- Familiarity with basic concepts of functional programming
- PhD degree (or be close to completion)
- Courage to learn and experiment with new techniques (Some theoreticians cannot stand the unpredictability of running experiments and waiting for their results)
- Eagerness and experience in collaborative theoretical research
- Must be able to communicate and work well with other team members
- Fluency in English, both orally and in paper writing
DESIRABLE SKILLS
The following skills are not at all mandatory. They however will be a plus
- Experience in functional programming
- Experience in algorithmic studies and experiments
- (Japanese language skills will be useful for everyday life, but not mandatory at all)
PRACTICAL
- This call was posted in October 2022. It will remain open until the position is filled.
(There is another researcher call that we are currently advertising. The current call may be closed early if we have a good candidate for this other call.) - Annual gross salary: JPY 4,260,000 — 7,368,000 yearly, gross (depends on qualifications and experience).
- The contract is initially until the end of a fiscal year (March 31), with the possibility of extension (maximum until the project ends in March 2025).
- Our admin staff will provide support for moving, visa application, etc.
- Starting date: as early as possible
- Location: Tokyo, Japan (remote work from abroad is not allowed)
APPLICATIONS AND INQUIRIES
Applications should be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Application (Category Theory).” Please include
- your brief CV,
- short description of research interests (can be very informal and short),
- the list of papers (a dblp or Google scholar link will do, for example),
- a couple of representative papers (in pdf), and
- (preferably) the contact of two references.
We will contact you for further material, provided that we find sufficient relevance in your application.
Inquiries should also be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Inquiry (Category Theory).”
LIVING AND WORKING IN TOKYO
We have employed 10+ researchers and scientific programmers from abroad–see our list of members/former members. We have ample experience in supporting them in coming to and living in Tokyo.
PRICES
Tokyo is not an expensive city. On actual prices and availabilities you will find a lot of information sources on the web (including this). Some sample prices:
- An studio apartment, 30m2, 30min door-to-door to our Tokyo site: JPY 80,000 / month
- A 2-bedroom apartment, 40m2, 20min door-to-door to our Tokyo site: JPY 130,000 / month
- A 15-min metro ride: JPY 200
- A quick (but nice) Japanese set meal: JPY 600-1000
- An exquisite sushi set meal (which even locals rarely have 🙂 ): JPY 30,000
- A pint of beer: JPY 800
APARTMENTS
You can easily find an apartment using the following websites: www.sabbaticalhomes.com, www.sakura-house.com/en, gaijinpot.com, and others.
LANGUAGE
The working environment is totally in English, with more than half of the team coming from abroad. Japanese language skills will help everyday life, but one can definitely live without them, as we know from our colleagues’ experience.