Subject area
Theory and Implementation of Agda

Subject area description
Research theoretical foundations and provide efficient implementations of dependently typed pattern matching in conjunction with subtyping, user-defined rewrite rules, and modal extensions of type theory.

Job assignments
The assignment will consist of research on type theory and its implementation, approximately 50 % of full time. The assignment will also consist of tasks within development, documentation, and maintenance of Agda, approximately 50 % of full time.

The work consists of developing efficient solutions for the implementation of type theory in a mathematically rigorous way; providing well-structured Haskell code for these solutions as extensions of the existing type theory implementation Agda; and documenting the obtained theoretical solutions and their realizations. Possible topics are dependently-typed pattern matching, subtyping, sized types, user-defined rewrite rules, and modal refinements of type theory (linearity, proof-irrelevance, meta-programming).

Eligibility
The qualifications for academic positions are given in Chapter 4, Section 3 – 4 of the Higher Education Ordinance.

An achieved doctoral degree is compulsory for a position as postdoctor. The doctoral thesis shall be in a relevant area according the the specific position stated in the advertisement, for example in computer science or software engineering. Since a position as postdoctor aims to give new holders of the doctorate the opportunity mainly to strengthen and develop their scholarly proficiency, we aim for those who have a doctoral degree not older than three years counting from the last date of application. Applicants with a degree obtained earlier than the stipulated three years may be preferred if special reasons exist.

Assessment
Regulations for the evaluation of qualifications for academic positions are given in Chapter 4, Section 3 – 4 of the Higher Education Ordinance.

Achieved a PhD in relevant research area. Several publications in international conferences and journals. Knowledgeable and experienced in using the above mentioned methods. Excellent skills in communicating both verbally and in writing.

The applicant should have solid experience with meta-theoretical work on dependent type theory and excellent knowledge of the Haskell programming language. Ideally, the candidate has worked and published on one or more of the following aspects of type theory: dependently-typed pattern matching, subtyping, sized types, user-defined rewrite rules, or modal refinements of type theory (linearity, proof-irrelevance, meta-programming).

Employment
Type of employment: Fixed-term employment, central agreement

Extent: 100%

Location: The department of Computer Science and Engineering

First day of employment: 2017-10-01

For further information:
Regarding the position please contact Head of Division Peter Dybjer, phone: +46 31 772 1035 or e-mail: peterd@chalmers.se

Regarding the appointment procedure, please contact HR-specialist Anna Skanse Bråse, phone +46 31 772 8167 or e-mail: anna.skanse@chalmers.se

Unions
Union representatives at the University of Gothenburg: http://www.gu.se/english/about_the_university/job-opportunities/union-representatives

How to apply
In order to apply for a position at the University of Gothenburg, you have to register an account in our online recruitment system. It is the responsibility of the applicant to ensure that the application is complete in accordance with the instructions in the job advertisement, and that it is submitted before the deadline. Reference number should be clearly stated when sending complementary documents.

The application is to be written in English. To apply, please follow the link;http://www.gu.se/english/about_the_u...etails/?id=986
Closing date: 2017-07-31