<div dir="ltr"><div dir="ltr">Dear Agda community,<div><br></div><div>I am writing to advertise a postdoc position working with me at Iowa on Cedille, a constructive type theory I and my trainees have been developing the past few years.  The main idea of Cedille is to use impredicative lambda-encodings with dependent elimination as the basis for inductive reasoning and dependently typed programming.  This means Cedille does not have primitive datatypes, so the trusted core is very small: it can be easily checked in under 1000 lines of Haskell.  Cedille is primarily implemented in Agda (hence the email to this list), with a little Haskell and a good bit of elisp.  </div><div><br></div><div>We have recently had a number of papers about encoding various forms of datatypes and recursion schemes in Cedille.  There is more to study there, including codatatypes and other forms of recursion.  This direction should lead to a number of further papers.  There are also foundational questions like how to add extensional concepts to Cedille that warrant investigation.  People recently working on the project have also found their own interesting topics to investigate.</div><div><br></div><div>I'd be very pleased to hear from those who have recently completed or are currently finishing their doctoral studies, who might be interested.  I am also open to inquiries from more established researchers.  The position is available now and I have funding from a grant in hand for it through end of November 2020 (so a little under two years).  Salary is competitive.</div><div><br></div><div>Thanks,</div><div>Aaron</div><div> </div><div>Aaron Stump</div><div>Professor</div><div>Computer Science</div><div>The University of Iowa</div><div class="gmail-yj6qo gmail-ajU" style="margin:2px 0px 0px"></div></div></div>