Personal Information

• Contact Information
• Travel Plan
• Curriculum Vitae
• Statement of Purpose (PDF, PostScript, DVI)
• Dissertation
• Picture
• PGP Public Key
• Finger

Useful Pages at Carnegie Mellon

• SCS Personal Home Pages
• Technical Reports On-line
• Lycos Internet Catalog
• Webster Dictionary

  Logical Frameworks

• Twelf
• Coq
• Hol
• Isabelle

  Twelf

• Source of a  preliminary version of TwelfX (unix, windows)
• Slides of a presentation of TwelfQ, the predecessor of TwelfX

Publications

• Higher-Order Superposition for Dependent Types (postscript file, 439607 bytes)
• An extended abstract of the above, accepted at RTA '96 (postscript file, 145923 bytes)

The Mathematica Corner

• An implementation of Knuth-Bendix completion (notebook, 41082 bytes)
• A theorem prover for first order logic based on rewriting techniques (notebook, 43529 bytes)
• The Peterson-Stickel completion algorithm for equational theories with associative-commutative operators (notebook, 53834 bytes)

A Cup of Java

• MineSweeper
• Typing Tutor
• WebCounter

Orchids

• Publications: American Orchid Society, The Orchid Digest, Botana
• Other sources of information: Weblopedia, Orchid Species Culture, Aaron Hicks' archive, Orchids of California
• Nurseries: Venger, Chula Orchids, HBI
• Miscellanea: Orchidmania SF, The Seedbank Project
• My orchids