Homepage of Robert R Schneck

Currently I am a member of Twin Oaks Community, which is an egalitarian income-sharing community in rural Virginia. I live there with my partner Thea Tupelo (née Krista Laffoon) and children Jonah (age 6) and Gwen (age 4).

Promethea Tupelo and Robert Schneck are getting married on October 6th, 2007!

I make cheese, clean the dairy barn, wash dishes, work on database programming, weave hammocks, pack tofu, garden, do accounting work, and I am also engaged in some part-time programming and research work with Google.

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.

I have developed some code to make it relatively easy to develop custom tree models using LablGTK in OCaml.

Research

Work in proof-carrying code

As of May 2004 I have 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, as well as 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. Someday I may try to ready it for publication.

Projects

I used to maintain some packages for Cygwin, which provides a Linux-like environment on computers running Windows.

My own Cygwin page is here, including especially advice and scripts for offline mail and news reading.

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.

Long ago I coordinated, through the de-cal program, UC Berkeley's course in Esperanto. If you want to study Esperanto at Berkeley, and cannot find more up-to-date information elsewhere, please contact me.

In the past I was married to Claire R McConnell. Socially we used the name Schneck-McConnell.

Last updated 2007-08-05.