Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Jobs combining type theory and web programming

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Jobs combining type theory and web programming


chronological Thread 
  • From: Adam Chlipala <adam AT chlipala.net>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>, agda AT lists.chalmers.se
  • Subject: [Coq-Club] Jobs combining type theory and web programming
  • Date: Sun, 06 Feb 2011 15:20:34 -0500

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.



Archive powered by MhonArc 2.6.16.

Top of Page