<div dir="ltr">PS I forgot to note that Cedille is implemented in Agda!<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, May 29, 2016 at 3:33 PM, Aaron Stump <span dir="ltr"><<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda community,<br>
<br>
I am writing to advertise a postdoctoral research position working with me on dependently typed lambda encodings, in the Computer Science department at The University of Iowa. The position is for two years, and the start date is flexible. Salary and benefits are competitive. The project is funded by the U.S. National Science Foundation.<br>
<br>
The project is to develop and evaluate Cedille, a new implementation of a system I am proposing called the Calculus of Dependent Lambda Eliminations (CDLE). CDLE is based on a version of the Calculus of Constructions (CoC) with implicit products (cf. Miquel's implicit CoC). This system is extended with new features supporting dependently typed programming with lambda encodings. These new features enable data to be defined to be their own inductions (so the type of 3 says that if you prove standard step and base cases for a property P, then you get a proof of P of 3), and allow large eliminations with such data. This system supports programming and proving with higher-order lambda encodings of datatypes with embedded functions; such datatypes are not allowed in Coq or Agda for consistency reasons. Nevertheless, CDLE is a sound logic under the Curry-Howard isomorphism, as higher-order lambda encodings (as possible already even in System F) do not jeopardize consistency. For more about this system, see the draft paper on my web page.<br>
<br>
If you are interested in applying for the position, please send an updated CV including the names of two references to me by email. Please also include preferred start date. A doctoral degree in Computer Science is required, and background in type theory, programming languages, compilers, or formal methods is strongly desired. Inquiries are also very welcome. I would be very happy to have applications from graduating students at institutions in Europe. Our Computational Logic Center here at U. Iowa, which I run together with my colleague Cesare Tinelli, has many international connections, including a number of current postdocs who completed doctoral training at schools in France and the UK.<br>
<br>
Sincerely,<br>
Aaron<span class="HOEnZb"><font color="#888888"><br>
<br>
Aaron Stump<br>
Professor<br>
Computer Science<br>
The University of Iowa<br>
</font></span></blockquote></div><br></div>