[Agda] postdoc opportunity on Cedille project

[Aaron Stump]

Dear Agda community,

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.

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.

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.

Thanks,
Aaron

Aaron Stump
Professor
Computer Science
The University of Iowa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190226/3f250b9e/attachment.html>