[Agda] Re: postdoc recruiting

[Aaron Stump]

PS I forgot to note that Cedille is implemented in Agda!

On Sun, May 29, 2016 at 3:33 PM, Aaron Stump <aaron-stump at uiowa.edu> wrote:

> Dear Agda community,
>
> 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.
>
> 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.
>
> 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.
>
> Sincerely,
> 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/20160529/e0d6b4fe/attachment.html