I currently live in Charlottesville where I program for CNRI on the Handle System and related topics.
I have worked on a preferential voting system for democratically distributing funds for projects; essentially this is a generalization of STV that, instead of electing candidates to a committee or body, elects projects to be funded. The funding levels for elected projects can all be different, and the voters determine not only which projects will be funded but also how much funding each will receive.
This work is in collaboration with Rob Loring. See his page on Fair-share Spending aka Movable Money Votes.
Inductive programming is programming by example. For example, you might tell an inductive programming tool you want a program which, given the input list [3, 1, 4, 1, 5], returns the output list [1, 1, 3, 4, 5]. The tool then returns with an implementation of a sorting algorithm. Inductive functional programming returns a program written in a functional language like ML or Haskell (instead of the more traditional logic language like Prolog). From 2004 to 2008 or so I worked with Jeremy Bem and Google on an inductive functional programming tool. (Thanks to the Curry-Howard isomorphism, it's also a mathematical theorem prover!)
See Jeremy's ongoing work: Formalpedia, Llama Labs, ZPC.
In May 2004 I graduated with a Ph.D from the Group in Logic and the Methodology of Science at the University of California, Berkeley. My advisor was George C. Necula of the Computer Science Division of Berkeley's Department of Electrical Engineering and Computer Science. My work was in proof-carrying code, specifically in the development of certain techniques to create more extensible and trustworthy proof-carrying code frameworks, which nonetheless retain the ability to scale to large programs. Working with us were Bor-Yuh Evan Chang and Adam Chlipala.
Before beginning my thesis work, I did some work in linear logic, studying the proof nets of two-negation non-commutative multiplicative linear logic, including the units and allowing additional axioms. Robin Cockett and Robert Seely encouraged me in this work.
I have developed some code to make it relatively easy to develop custom tree models using LablGTK in OCaml.
I used to maintain some packages for Cygwin, which provides a Unix-like environment on computers running Windows. I still have some mostly outdated advice about using Cygwin.
Some years ago I wrote “Another ScottFree Driver” which allows one to play the old (circa 1980) Scott Adams adventure games. It fixed some bugs in the then-existing driver and fulfilled my main goal of giving VIC-20 look-and-feel. Driver and games available here.
I live with my wife Promethea (Thea, née Krista Laffoon) and children Jonah (age 11), Gwendolyn (age 9), and Henry (born 2010-01-28). We were married on October 6th, 2007.
(I was born with the name Schneck and acquired the name Tupelo at marriage. Previously I have worked under the name Schneck-McConnell.)
I have been a member of Acorn Community and Twin Oaks Community, egalitarian income-sharing communities in rural Virginia. I have worked in database design and maintenance for Southern Exposure Seed Exchange and Turtle Tree Biodynamic Seed Initiative.