hacker // trader // researcher // engineer

Research interests include functional programming, dependent types, constructive mathematics, type theory, and category theory.

Much of my time is spent at the moment in Agda and Coq working on formalized categorical models of higher dimensional type theory.

Interested in engineering tasks for which the above topics are relevant, particularly applications in defense, quantitative finance, and security.

I work on Mac OS X and sometimes Linux. I use Emacs and Sublime Text 2 as my editors.

More info:

http://www.github.com/darinmorrison
http://www.linkedin.com/profile/view?id=154451640