From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10834 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Ichiro Hasuo Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.categories,gmane.science.mathematics.logic.coq.club Subject: Postdoc & Scientific Programmer Positions in Tokyo Date: Sun, 30 Oct 2022 15:35:42 +0900 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============0295847524419569454==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="28284"; mail-complaints-to="usenet@ciao.gmane.io" To: types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, pvs-1VPwtPCARB1BDgjK7y7TUQ@public.gmane.org, hscc-bGTZWsvkwUHhn2KNwJGQxje48wsgrGvP@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Sun Oct 30 10:28:23 2022 Return-path: Envelope-to: gcst-types-announce@m.gmane-mx.org Original-Received: from mx0a-00390e01.pphosted.com ([148.163.133.158]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1op4cA-00076y-F5 for gcst-types-announce@m.gmane-mx.org; Sun, 30 Oct 2022 10:28:22 +0100 Original-Received: from pps.filterd (m0172791.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.17.1.5/8.17.1.5) with ESMTP id 29U8wG7E019989; Sun, 30 Oct 2022 05:27:29 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com (PPS) with ESMTP id 3khhge1wdm-1; Sun, 30 Oct 2022 05:27:29 -0400 Original-Received: from rhizome.seas.upenn.edu (RHIZOME.SEAS.UPENN.EDU [158.130.69.24]) by leopard.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 29U9RMQ9080302; Sun, 30 Oct 2022 05:27:22 -0400 Original-Received: from RHIZOME.SEAS.UPENN.EDU (localhost.upenn.edu [127.0.0.1]) by rhizome.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 29U9RMHr074789; Sun, 30 Oct 2022 05:27:22 -0400 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from mx0b-00390e01.pphosted.com (mx0b-00390e01.pphosted.com [148.163.137.158]) by rhizome.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 29U6Ztbv062186 for ; Sun, 30 Oct 2022 02:35:55 -0400 Original-Received: from pps.filterd (m0172794.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.17.1.5/8.17.1.5) with ESMTP id 29U6DYx5014177 for ; Sun, 30 Oct 2022 02:35:55 -0400 Original-Received: from mail-yb1-f182.google.com (mail-yb1-f182.google.com [209.85.219.182]) by mx0b-00390e01.pphosted.com (PPS) with ESMTPS id 3khhgu8y7w-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Sun, 30 Oct 2022 02:35:55 -0400 Original-Received: by mail-yb1-f182.google.com with SMTP id 185so10526955ybc.3 for ; Sat, 29 Oct 2022 23:35:54 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=to:subject:message-id:date:from:mime-version:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=bux9m0Al9Gi9bX4t2hRiG0zPk1/ON/Qptv0Awx5N7ps=; b=t6DpRavkTFuC8Nrk2XHy679qkc8iH8dw5qJ0BUAKC605XP9JhvLZCPYXkWhjoCsRIX YkBcBx4LN+c4dZq01VygqotttlZ22Q7ksnl+iVy9ayugC+Fgqd/wDe2mnjX4KpvxInJs cx6pAgyoeBuRB7cU44RLz3Q+VeDYRBiFbuiYLp0I3kRR63nx9IbSZMEN8PZsVbq84CDU DvEjAY33aklGICexszh43eebVS9BkNLIIMuItmKZDsrNE8HydkIjWEDqhjFAzI9Ev5F/ 86tz/f5TrCCsQP2wOHF5OEXSFBZ6xzt7voFwS8g5Th/ntzScOe9G78oBFoHWHYavusSp L+6w== X-Gm-Message-State: ACrzQf3/XwPdYMObXp7FSZwfGeMQqNN+my7Q4m1e+oVaAQQNnq1h96c3 qOUBy0zi2Z7U39DLdYB/xddxyKRf1Ed3dKF12iveBoybhHr2Hg== X-Google-Smtp-Source: AMsMyM7vtY2LBFQ1C1Y6b70Rrt1IO1J7u2+lLYd9hUSNvmhuNLRu+JbmkOrlQXU6nYHx/d/g/JxMtwnVRsLigjMta0A= X-Received: by 2002:a25:bb4c:0:b0:6c1:e145:d68a with SMTP id b12-20020a25bb4c000000b006c1e145d68amr7094739ybk.338.1667111753932; Sat, 29 Oct 2022 23:35:53 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.895,Hydra:6.0.545,FMLib:17.11.122.1 definitions=2022-10-30_01,2022-10-27_01,2022-06-22_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 malwarescore=0 clxscore=180 suspectscore=0 adultscore=0 phishscore=0 lowpriorityscore=0 bulkscore=0 mlxscore=0 impostorscore=0 priorityscore=0 spamscore=0 mlxlogscore=772 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2210170000 definitions=main-2210300042 domainage_hfrom=11216 X-Mailman-Approved-At: Sun, 30 Oct 2022 05:27:17 -0400 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.35 Precedence: list List-Id: Announcements of interest to the TYPES community List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Original-Sender: "Types-announce" X-Proofpoint-ORIG-GUID: 8DaOstudNZgJoNq8e_j9K1ZFM3oS25Nk X-Proofpoint-GUID: 8DaOstudNZgJoNq8e_j9K1ZFM3oS25Nk X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.895,Hydra:6.0.545,FMLib:17.11.122.1 definitions=2022-10-30_03,2022-10-27_01,2022-06-22_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 bulkscore=0 clxscore=1011 adultscore=0 lowpriorityscore=0 priorityscore=1501 mlxlogscore=999 suspectscore=0 impostorscore=0 spamscore=0 malwarescore=0 phishscore=0 mlxscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2210170000 definitions=main-2210300061 Xref: news.gmane.io gmane.comp.science.types.announce:10551 gmane.science.mathematics.categories:10834 gmane.science.mathematics.logic.coq.club:23163 Archived-At: --===============0295847524419569454== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --===============0295847524419569454== Content-Type: multipart/alternative; boundary="000000000000e4e2a305ec3ab384" --000000000000e4e2a305ec3ab384 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable [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://urldefense.com/v3/__https://group-mmm.org/eratommsd/call-for-studen= ts-ja/__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iU= zY7_4-wdk1NsywhboVjSTrusXj2F89a4ZHvj$=20=20 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-researc= her-category-theory-and-practical-model-checking-algorithms-oct-2022/__;!!I= BzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1Ns= ywhboVjSTrusXj2F87q9uph3$=20=20 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/97= 8-3-031-13185-1_12__;!!IBzWLUs!TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMX= KBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F8793XR6J$=20=20 - Komorida et al., LICS'21 https://urldefense.com/v3/__https://arxiv.org/abs/2105.10164__;!!IBzWLUs= !TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboV= jSTrusXj2F80a4wpFf$=20=20 ---- Position 2: PostDoc Researcher, Theorem Proving for Automated Driving https://urldefense.com/v3/__https://group-mmm.org/eratommsd/postdoc-researc= her-theorem-proving-for-automated-driving-oct-2022/__;!!IBzWLUs!TFlcPMXSygs= 1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTrusXj2F8-= XvAwjS$=20=20 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-wdk1NsywhboV= jSTrusXj2F82tBPpkZ$=20=20 ---- Position 3: Scientific Programmer towards a Research-Oriented Startup https://urldefense.com/v3/__https://group-mmm.org/eratommsd/open-position-f= or-a-scientific-programmer-towards-a-research-oriented-startup/__;!!IBzWLUs= !TFlcPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboV= jSTrusXj2F81AQ0dzW$=20=20 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! =3D=3D=3D=3D=3D=3D 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!TFl= cPMXSygs1uyMkZ3cDFTVaozt6ZEWvuji-pdNbWAMXKBdRqVEqr4iUzY7_4-wdk1NsywhboVjSTr= usXj2F86jT7V9U$=20=20 --000000000000e4e2a305ec3ab384 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable
[Please distribute, apologies for multiple postings.]
=
Open=C2=A0Postdoc & Scientific Programmer Positions in T= okyo

Hasuo Laboratory<= /a> at the National Institute of Informatics, Tok= yo, Japan invites applications for a scientific programmer and a postdoc re= searcher. The positions are funded by a JST ERATO project (scientific resea= rch) and a JST START project (practical development towards a research-orie= nted startup), and their scopes are largely=C2=A0the application of foundat= ional research on logic and semantics to real-world=C2=A0problems. See belo= w for the specific scope of each position. The positions are for ~2.5 years= max.

We are also constantly looking for PhD stude= nts.=C2=A0https://group-m= mm.org/eratommsd/call-for-students-ja/

Thanks = a lot for your consideration.
Best, Ichiro


----=C2=A0
Position 1:=C2=A0

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

Key publications:=C2=A0


----=C2=A0
Position 2:=C2=A0
PostDoc Resear= cher, Theorem Proving for Automated Driving

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

Key publication:=C2=A0<= /div>


----=C2=A0
Position 3:= =C2=A0
Scientific Programmer towards a Research-Oriented Startup<= /div>

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


=3D=3D=3D=3D=3D=3D
Ichiro Hasuo
Professor, Natio= nal Institute of Informatics
i.hasuo-HInyCGIudOg@public.gmane.org =C2=A0 =C2=A0 Secretaries: hasuolab-secr-5aC7G4kDdWR4Eiagz67IpQ@public.gmane.orghttp://group-mmm.org/~ichiro= /
--000000000000e4e2a305ec3ab384-- --===============0295847524419569454==--