coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] PhD position in Type Theory at Chalmers/Gothenburg University (deadline 8 Nov)

From: Andreas Abel <abela AT chalmers.se>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] PhD position in Type Theory at Chalmers/Gothenburg University (deadline 8 Nov)
Date: Thu, 21 Oct 2021 21:42:35 +0200
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 129.16.226.133) smtp.rcpttodomain=inria.fr smtp.mailfrom=cse.gu.se; dmarc=none action=none header.from=chalmers.se; dkim=none (message not signed); arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=KJztYcI97hszRuzHnLZZr5hnzKPLaGM8cB6Aql11JBU=; b=JiTb+VBKZnVbR6cktelmj8OcvHw3UIBLfcrSYnNzdJGNdhPvntHAWazbfWve4cC6OBoPi27Ifgs3G0NiOy9rU9z8AwmuYLY9WSextlO5xSXUX9fqppUG07yAgbYM342DKlnNlbSReC0dWUUrqcG9xuEDquZFVi9xY+DVlVZQPQeimAv5q7d4pNOmNB1K43q6cQFYcXkC8qWCg8WTT6D/NnWCN7CJIjDMdhHtqqKcJYyUAymFXIl0rZYH9Xsl/Irl/ICbLEWyayfu9398CAQ5OAzbZufwEQphdQZ37mgybA3RZdAUazYm3dMtISl+kErvpR5WhUREl/lGzp9pOnm9RQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=BKmiSGhQhesop8p0enRs9o/XJuDsgXeEiwHjTkc2ZVUlubOqycxEvdmmtjegjqmBKFv73A6JXsNVeK5gpKdiPOSGrtT1slqNAnZgZBbVeTgzvNQz1rVvYIMJyDpo4bmeIi3zPz85kTv2c5Ubn1addb+/IYUpMbfxDFqYiWBdCt3NpiR+7svyvgjQ+9eeeA6CQlUhxdPlJPMm7gHaI4LJkS4gBPpYOcQdIEfToyp9hi20R86a3SwByqGKdxF5Bhca7i4nNzcNDY+OhzsBXi1vgce9SR1Qo8ZuRNRx1MJJufPOfvzgWHCq+qs0PXeVlwdIndFFuABAx140ubuMrtSw1g==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abela AT chalmers.se; spf=Pass smtp.mailfrom=andreas.abel AT cse.gu.se; spf=Pass smtp.helo=postmaster AT EUR02-HE1-obe.outbound.protection.outlook.com
Ironport-hdrordr: A9a23:UMYsFa1yjac9J9H8+26WrwqjBK8kLtp133Aq2lEZdPU1SL36qynApoV/6faZslgssRIb+exoRpPwI080nKQdieJ6AV7FZmjbUQCTQL2Kg7GO/9SZIULDytI=
Ironport-phdr: A9a23:YMpCMhxaUOuujrTXCzKszVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+ZhSZtKwm0QCBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdi72/q29pHObAlFhDiwaq5uIRurqgncqtMYipZ4JKYrzRvJrHpIe+BIym5tOFmegRXy6Nqu8ZB66yhftO4v+MBGUaXhYqQ3VqdYAyg8M2A0/8Lkqx/ORhaS63QGU2UWlh1IAxXZ7Bz/Q5z8vDf2uvZ71SKHOsL4UK00WS+676h1VBDolCkJNzk88G7Ni8xwir9QrBauqhF7xoLZZpyeOvhjcaPHZd4URmRPUclfWCJBH42ycZcAAeUAPetDs4nwpUEDoQeiCQSiBu7izCJDiH/s3a091uQsCR3L3Ao9ENIUrnvbts71P7oOXO+u0qbIySjIYvRM1jjm9ofIdgourOqQUrJwa8XRzUwvGB3fjlWLs4DlJC2a2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HGiI8Wyl3I6yV3zYg1K9CkRkB2fMOoHZpQuS2GNoZ4TMwsTWFmtSs4ybALuoC3cDQWxZkp2xPSdv6KfYeL7x/hUuuaPDl2hHVgeL2lhhay91Ctxfb9VsmoylpKqipEnsHQuXANzRPT7s2HReVn/ke6wzqPzB7c5+dZKk43jarWM5EszqIqmpYOrUjOHDX6lFjsgKOLakko5vCk5/n5brjivJOQKo55hhvjPqgygMCzH+s1PwgIUmOG4+qzzqfj8lf8QLhSjv05jK3ZsJfCKMoUqKG3HxNZ3pg65xi9ADmqzc0UnX4cI11bYh6HiJXpO03VL/D/EPe/hUmjnC1zx/DcOb3hHovCIWTfkLfgerZ97VRQyA0uzdBD45JUDbYBIPHpVkDts9zYCwc1Mw2yw+n5FNVwzowTVX6VDqOELK/fs0WE6v81L+WReIMZpC7xK/0/6P7viX85l0Udfa6s3ZYPcn+4GOlpI1+HbnX2mdcNC30FsREgQ+zuk1CNTSVTaGioU6Iz+zE3EpmmApnbSoC3nLOBxDu7HoFRZm1eFl+MFm7oe5yYVPcIdSKdOdRskicEVLikU48uzwuitA78y7p9L+rb4DcUtZz51Is92+qGwRo17Hl/C9mX+2CLVWB92G0SEWwYxqd69GV7xk2O2LMwqvZVEZQH7vlEVg4SPp7Vy+l3Ecu0QQ+XLYTBc0qvXtjzWWJ5ddk22dJbPxcV8zSKoy35h3DvI5JM0ruBCdoz777W2GX3K4Bl0XHa2aI9jl4gBMxSKWmhga05/A/WVdehe6CxnKajcaERxjWL72rRlQJmU2lTSwM2XriDRn1NPyPr

We are opening a PhD position in the Logic & Types unit of the
Department of Computer Science and Engineering joint at Chalmers and
Gothenburg University.

Ad : Doctoral student in Logic and Types:
Theory and implementation of dependent types
URL: https://bit.ly/3m0lmP6

Apply until: 8 November 2021

This position is a great opportunity for you as a PhD student to
develop your scientific and technical skills as part of a team of
leading researchers in the area of dependent type theory and
implementors of the Agda proof assistant.

Logic & Types members:

https://www.chalmers.se/en/departments/cse/organisation/LT/Pages/Staff.aspx

The project aims to advance type theory both theoretically and
practically, in particular in the direction of modalities.
You will be working on type theory from a mathematical perspective
(type systems and their models), an algorithmic perspective
(unification and type-checking), and a programming perspective
(efficient implementation as part of the Agda proof assistant).

The position is for 5 years and comes with full benefits (pension
benefits, health insurance etc).
(Sweden is a good country for PhD students!)

For the full description, eligibility, documents required for the
application, see

https://bit.ly/3m0lmP6

Further questions can be directed to me,

Andreas Abel

P.S.: Colleagues, please advertise this position to suitable
candidates (e.g., your best students).

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www.cse.chalmers.se/~abela/

[Coq-Club] PhD position in Type Theory at Chalmers/Gothenburg University (deadline 8 Nov), Andreas Abel, 10/21/2021