Homepage of Robert R Tupelo-Schneck

I currently live in Charlottesville where I program for CNRI on the Handle System and related topics.

Recent projects:

• it's electric: software for storing and viewing home energy monitoring data
• Convex regular-faced polyhedra with conditional edges

Research and Projects

Fair-share Spending

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 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). 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.

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.

Personal

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.