From The Twelf Project
My name is Robert J. Simmons. I am a first-year graduate student at Carnegie Mellon University.
- Web page: http://www.cs.cmu.edu/~rjsimmon/
- Wikipedia: w:User:Sirmob
- Girard Reading Group Wiki: http://locuspocus.hyperkind.org/
I am the background maintainer for this website, and moog lives in my office. I developed the the TwelfTag extension for syntax highlighting automatically checking included Twelf code, the Literate Twelf extension to facilitate offline editing, and generally attempt to keep things working. Leave me a message if anything needs to be done.
 Scratch space
Since writing Literate Twelf, I tend to incorporate the Wiki into my development process. Often I only use the preview feature, but sometimes I save drafts in my namespace. Some of these would probably make good case studies if I get around to it.
- User:Rsimmons/primop.elf - Broken.
- User:Rsimmons/Subtype - Incomplete - an attempt at doing a reasonable encoding of (width,depth) subtyping for n-ary tuples.
- User:Rsimmons/Handled exceptions - An encoding of exceptions where the type system can statically determine code to be non-exception-raising.
- User:Rsimmons/Fluid binding - A more organized example than handled exceptions. This encodes "deep binding," requiring the dynamic semantics to search the stack for the correct binding; the type system ensures that some binding will be found. I was worried that the unsatisfactory encoding of sets would run into trouble, but it's actually a very context-like encoding of sets of fluid variables (weakening and exchange need to be proven explicitly, etc etc). This is the first encoding where I've wanted "Twelf functors" to abstract over the variable names - I can't use hypotheticals because I need decidable equality/inequality.