[Agda] Jobs combining type theory and web programming

[Adam Chlipala]

Some might argue that you can derive False from a sentence containing 
both "dependent types" and "contract programming."  I'm writing to 
provide evidence to the contrary, as I'm looking for collaborators on a 
commercial venture where I'm trying to bring ideas from 
dependently-typed programming into the real world.

For a few years, I've been working on the Ur/Web domain-specific 
language for web application programming:
     http://www.impredicative.com/ur/
Ur is a core language that starts from a subset of CIC that drops type 
dependency but keeps some of the interesting type-level computation 
possibilities.  A heuristic type inference engine tuned to this subset 
makes it possible to write interesting metaprograms with two key properties:
     1) Metaprograms rarely need to include proof terms.
     2) Application code rarely needs to include type annotations at 
metaprogram invocations.
Metaprogramming is very popular in the mainstream web frameworks, with 
programs generating application skeletons automatically, based on inputs 
like database schemas.  In Ur/Web, such generators may be type-checked 
independently of specific inputs, with strong guarantees about 
correctness and security.  There are also interesting things going on 
with abstraction and modularity, based on what you get when you combine 
strongly-typed encodings of SQL and XML syntax with ML-style modules and 
Haskell-style type classes.

I have been designing the language and its toolset to scratch itches I 
have felt while doing web programming.  This is a hybrid of a research 
project and a practical tool.  To further that second bit, I've been 
working on using Ur/Web in real commercial engagements.  I'm pleased to 
report that, in 2011, I have infinitely more such customers than I did 
in 2010.

This brings me to the point of the message: I'm looking for 
collaborators who are interested in doing various commercial things with 
Ur/Web.

I have one paying customer now for whom I'm doing contract programming, 
with an opportunity to bring a paid full-time programmer into that 
project more or less immediately.  I'm interested in trying to expand 
this sort of business; I want to take over the world of web programming 
and prove that advanced type system stuff is a killer competitive advantage.

I'm also keen on the idea of getting involved with start-up company 
efforts that would like a secret weapon for building high-quality web 
applications more effectively than the competition can.

If any of this sounds interesting, please e-mail me.  I would like to 
get in touch both with folks who would consider pursuing this sort of 
thing full-time, and with people like me who are mostly interested in 
doing research but also want to put in some time on "technology 
transfer."  The project has so far generated two research papers at top 
conferences, and I'm hoping for more of the same, based on experience 
gained with real-world applications.