For various reasons, I'm taking some time off from school. I'm looking for some interesting work for anywhere from 3 to 6 months--maybe more.
I specialize in programming languages: DSLs, static analysis, verification, program synthesis[1] and so on.
Admittedly, this is a narrow field, but it's also surprisingly broadly applicable: there are many domains where a small domain-specific language can be much more expressive than a standard library; I then know how to build some powerful tools on top of the language including things like bounded verification and all sorts of static checking. DSLs can be used both to help expert programmers or to make a system more accessible to non-programmers. Especially for the latter, we can also design interesting interactive tools that help non-experts express themselves as they go along.
I also do a lot of functional programming: primarily Haskell along with OCaml and Racket. If you're interested in experimenting with functional programming at your startup, I'd really love to help. Apart from actually using functional programming, I really enjoy teaching people about it: for example, I'm in the top 10 for [haskell] on StackOverflow[2] and I've recently been teaching people about type theory at a meetup in SF[3]. I also have a particular interest in functional reactive programming (FRP); over the summer, I even designed an FRP library for OCaml (in the browser--with js_of_ocaml).
I'd prefer to find something in the Bay Area, but I'm flexible along both remote work or living somewhere else.
[1]: Program synthesis is a type of automatic programming--generating programs programmatically, by searching through the space of all possible programs. It's an exciting field that has really heated up in the last few years thanks to advances in computational power and SMT solvers. I think it's about ripe for some practical applications. I've done some research on the subject and implemented a few different synthesizers, so I have a reasonably rare amount of experience with it.
Program synthesis also involves verifying the programs we generate. Our approach to "bounded verification" is actually interesting on its own: we can reasonably quickly check conditions against code exhaustively, using an SMT solver. This could be very useful if you need high levels of assurance about your code.
A fellow tinkerer in program synthesis? Just today, I was tweaking my AI-Programmer project http://primaryobjects.com/CMS/Article149.aspx, which uses genetic algorithms to generate programs.
Glad to see I'm not the only one who thinks programmers can/should become obsolete. :)
For various reasons, I'm taking some time off from school. I'm looking for some interesting work for anywhere from 3 to 6 months--maybe more.
I specialize in programming languages: DSLs, static analysis, verification, program synthesis[1] and so on.
Admittedly, this is a narrow field, but it's also surprisingly broadly applicable: there are many domains where a small domain-specific language can be much more expressive than a standard library; I then know how to build some powerful tools on top of the language including things like bounded verification and all sorts of static checking. DSLs can be used both to help expert programmers or to make a system more accessible to non-programmers. Especially for the latter, we can also design interesting interactive tools that help non-experts express themselves as they go along.
I also do a lot of functional programming: primarily Haskell along with OCaml and Racket. If you're interested in experimenting with functional programming at your startup, I'd really love to help. Apart from actually using functional programming, I really enjoy teaching people about it: for example, I'm in the top 10 for [haskell] on StackOverflow[2] and I've recently been teaching people about type theory at a meetup in SF[3]. I also have a particular interest in functional reactive programming (FRP); over the summer, I even designed an FRP library for OCaml (in the browser--with js_of_ocaml).
If any of this sounds interesting, I'd love to talk to you! My email is tikhon@jelv.is; you can see a recent resume at http://jelv.is/resume.pdf or on http://careers.stackoverflow.com/tikhonjelvis. My site, naturally, is http://jelv.is; I have to admit I'm unreasonably happy with the little domain hack :). Also check out my LinkedIn profile: http://www.linkedin.com/pub/tikhon-jelvis/24/237/750
I'd prefer to find something in the Bay Area, but I'm flexible along both remote work or living somewhere else.
[1]: Program synthesis is a type of automatic programming--generating programs programmatically, by searching through the space of all possible programs. It's an exciting field that has really heated up in the last few years thanks to advances in computational power and SMT solvers. I think it's about ripe for some practical applications. I've done some research on the subject and implemented a few different synthesizers, so I have a reasonably rare amount of experience with it.
Program synthesis also involves verifying the programs we generate. Our approach to "bounded verification" is actually interesting on its own: we can reasonably quickly check conditions against code exhaustively, using an SMT solver. This could be very useful if you need high levels of assurance about your code.
[2]: http://stackoverflow.com/tags/haskell/topusers
[3]: You can see past slides at http://jelv.is/talks. Feel free to pop by our next meeting about two weeks from now; we're going to have an introduction to basic category theory, with very little mathematical background needed. The actual meetup page: http://www.meetup.com/SF-Types-Theorems-and-Programming-Lang...