[Agda] postdoc recruiting

[Aaron Stump]

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