[Agda] PhD positions with Cogent and Trustworthy Systems

[Liam O'Connor]

Hi all,

If you have (or are) a promising undergraduate or masters student who would be interested in working with us on the lovely intersection of programming languages and formal methods, my colleague Christine has recently begun looking for PhD students. 

The ad is attached below. Both of us will be in Berlin for the rest of the week (after ICFP), so feel free also to talk to us in person if you are around.

Liam
—

If only there were a place where I could prove theorems, change the world, and have 
fun while doing it... 

Sounds too good to exist? 

In the Trustworthy Systems team at UNSW and Data61 that's what we do for a living. We 
are the creators of seL4, the world's first fully formally verified operating system 
kernel with extreme performance and strong security & correctness proofs. Our highly 
international team is located on the UNSW campus, close to the beautiful beaches of 
sunny Sydney, Australia, one of the world's most liveable cities. 

We are offering scholarships to multiple motivated PhD students who want to join us 
in Sydney, move things forward, and have a global impact. 

Cogent is a language we designed that co-generates code and proofs in order to ease 
the verification of systems components around seL4. Potential PhD topics include 
designing and implementing new domain-specific programming languages extending 
Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally 
verified infrastructure for building secure systems on top of seL4, contributing to 
improved proof automation and reasoning techniques, and applying formal proof to 
real-world systems and tools. 

To apply you should have (or be about to obtain) a bachelor degree (minimum 4 years) or 
a bachelor and a masters degree in Computer Science, Mathematics, or similar. You should 
also meet UNSW's minimum English requirements: 
https://www.unsw.edu.au/english-requirements-policy 

You should also possess a significant subset of the following skills: 
- functional programming in a language like Haskell, ML, or OCaml 
- first-order or higher-order formal logic 
- basic experience in C 
- ability and desire to quickly learn new techniques 
- ability and desire to work in a larger team 

If you additionally have experience 

- in software verification with an interactive theorem prover such as 
Isabelle/HOL, HOL4, Coq, or Agda, and/or 
- with programming languages and verified or certifying compilers 

you should definitely apply! 

You will work with a unique world-leading combination of OS and formal methods 
experts, students at undergraduate and PhD level, engineers, and researchers from 
5 continents, speaking over 15 languages. 

Trustworthy Systems is a fun, creative, and welcoming workplace with flexible 
hours & work arrangements. 

We value diversity in all forms and welcome applications from people of all ages, 
including people with disabilities, and those who identify as LGBTIQ. See 
https://ts.data61.csiro.au/diversity/ for more information. 


For applying, email us on <c.rizkallah at unsw.edu.au> a copy of your CV, 
cover letter, transcripts, and contact information for two referees. 


This round of applications closes on the 1st of September 2019. 


For any questions on these positions, please contact Christine Rizkallah 
<c.rizkallah at unsw.edu.au> 

The Cogent project is open source. 
Check it out at https://ts.data61.csiro.au/projects/TS/cogent.pml 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190822/d4b2a954/attachment.html>