|
|
Bio
I'm a fourth-year (yikes!) Ph.D. student in the POP Group of the Computer Science Department in the School of Computer Science at Carnegie Mellon University (whew!). In a former life, I was an undergraduate in the School of Engineering and Applied Science at the University of Pennsylvania, where I majored in Computer Science and Engineering and Cognitive Science.
Research
I'm interested, broadly, in the theory of programming languages, including type systems, constructive logics, mathematical philosophy, and inventing pretty syntax. Someday I hope to fill this section with many interesting results in these areas. (Watch this space! --> <--)
I am advised in my pursuits by Frank Pfenning, patron saint of Logical Frameworks.
Refereed publications:
- A Bidirectional Refinement Type System for LF.
William Lovas and Frank Pfenning.
Second International Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice (LFMTP '07).
Electronic Notes in Theoretical Computer Science,
Volume 196, pp. 113-128, January 2008.
( paper: pdf, bibtex / tech report: pdf, bibtex / talk: ppt2003, pdf )
Other writings:
- Thesis Proposal: Refinement Types for LF.
William Lovas. May 2008.
( document: pdf / talk: pdf ) - A Programming Language Based on Classical Logic.
William Lovas. Speaking Skills Talk. May 2008.
( talk: pdf )
Structural Normalization for Classical Natural Deduction. William Lovas and Karl Crary. Draft, December 2006.
( paper: pdf )
Some interesting PL conferences' archives in the ACM Digital Library:
Teaching
In the Fall of 2006, I TA'd 15-814, Type Systems for Programming Languages, a CMU star-course that might best be described as ``a very simplest introduction to the science of clear thought''.
In the Fall of 2005 I TA'd 15-501/15-819, HOT Compilation, a revolutionary new course on higher-order, type-preserving compilation. This is the wave of the future in compilation technology!
Links
- My old internet homesite, c/o flamingtext.com and my officemate, Tom 7. Variously described as "vastly superior" and "flaming".
- The ConCert Reading Group, a PL-oriented discussion group that I help maintain along with Spoons
- Various colleagues, cohorts, and partners-in-crime:
- My officemate Tom 7, an all-around wacky guy
- Spoons, my go-to guy on all things gourmet
- Fellow 2004-enterer, Little Dan
- Crazy monad man and clf luminary, Neel
- Category-theorist extraordinaire, jcreed (also, most likely to ask where my list of lleagues and horts is)
- Girard enthusiast, Noam
- Another one of my officemates, and general German guy, Kevin Bierhoff-Verlag
| May 24, 2008 | S (SKK) (SKK) (S (SKK) (SKK)) |