Homepage of Robert R Tupelo-Schneck

Currently I am a member of Twin Oaks Community, which is an egalitarian income-sharing community in rural Virginia.

I do some freelance programming and database design. Currently I am working on a project for FairVote and with Turtle Tree Biodynamic Seed Initiative.

Until late in 2006 I was a member of Acorn Community; I still do some work with their mail-order seed company, Southern Exposure Seed Exchange.

My resume. I am actively seeking full-time employment in or near Charlottesville.

Research

Movable Money Votes (MMV)

I am actively working 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 MMV.

Inductive functional programming

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). I've spent some time working with Jeremy Bem and Google on an inductive functional programming tool. (Thanks to the Curry-Howard isomorphism, it's also a mathematical theorem prover!)

Work in proof-carrying code

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.

• With Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. The Open Verifier Framework for Foundational Verifiers. In the proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '05), 2005.
• With Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. Type-Based Verification of Assembly Language for Compiler Debugging. In the proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '05), 2005.
• My dissertation, Extensible untrusted code verification. Filed May 2004.
• With George C. Necula. A sound framework for untrusted verification-condition generators. In the proceedings of LICS 2003, the IEEE Symposium of Logic in Computer Science, July 2003.
• With George C. Necula. Proof-carrying code with untrusted proof rules. In M. Okada, ed., Software Security---Theories and Systems; Mext-NSF-JSPS International Symposium, ISSS 2002, Lecture Notes in Computer Science, 2003.
• With George C. Necula. A gradual approach to a more trustworthy, yet scalable, proof-carrying code. In A. Voronkov, ed., Automated Deduction---CADE-18, pages 47-62, Lecture Notes in Computer Science, July 2002.
  • This paper references formal proofs implemented in the Coq proof assistant; these proofs are available here.

Older work in linear logic

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.

• Natural deduction and coherence for non-symmetric linearly distributive categories. Theory and Applications of Categories 6 (2000) 105--146.
• The just-mentioned paper mentions a very nice proof-net criterion for non-commutative proof nets; I have a long-neglected paper which proves the correctness of this criterion.

Various Projects

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 used to speak Esperanto.

Personal

I live with my wife Promethea (Thea, née Krista Laffoon) and children Jonah (age 7) and Gwen (age 5). 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.)

Last updated 2008-08-21.