The Coq mailing list

[Mateus de Oliveira Oliveira <mateus.oliveira AT gmail.com>]

Call: 

Applications are sought for a short-term internship in proof formalization at the University of Bergen. 

International students are also welcome to apply. The student will be conducting his/her project at the

Department of Informatics (Algorithms Group). 

The internship will occur in the context of the project 

AUTOPROVING: Automated Theorem Proving from The Mindset of Parameterized Complexity Theory

Topic: 

The topic of the internship is "Formalization of dynamic programming algorithms in the Coq proof assistant". 

Essentially we will provide very detailed inductive proofs of correctness for certain parameterized dynamic

programming algorithms and the task of the student will be to formalize these proofs in the Coq proof assistant. 

The student should have excellent skills in the Coq proof assistant. No previous knowledge of parameterized

algorithms is required.

Financial support: 

We will reimburse expenses with the following: 

1) return flight/train tickets between your location and Bergen.  

2) accommodation.

3) basic local expenses.

Duration and Starting Dates:

Ideally, the internship should last between 1 and 3 months. Ideal starting dates are December 6, 2021,

or January 10, 2022. But starting dates and duration are flexible. 

Application:  

If the internship described above sounds interesting to you, 

please send the following information, in a single PDF file, to  

mateus.oliveira AT uib.no . Please write INTERNSHIP in the subject field. 

1) A short application letter describing your skills in the Coq proof assistant. At most one page.

2) Your CV. 

3) Your Grades. 

7) Estimated starting-finishing dates.

8) A cost estimate, including the cost for a return ticket between your

location and Bergen, and the cost for accommodation in Bergen.

Deadline: 

The application deadline is November 26. Nevertheless, the selection will occur on a continuous

basis until the internship positions are filled. So we recommend not waiting until the deadline for

your application. 

More Information: 

Please feel free to send inquiries to mateus.oliveira AT uib.no

Best Regards, 

Mateus

-----------------------------------------------------------------------------------------------------------------------------------------------

Mateus de Oliveira Oliveira

Researcher

University of Bergen - Department of Informatics

mateus.oliveira AT uib.no

https://autoproving.org/mateus-de-oliveira-oliveira