|
|
Bio
I'm a recent Ph.D. graduate from 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.
My recent work has focused on adding refinement types to the logical framework LF. Refinement types offer expressive means like subtyping and intersection types to ease the encoding of certain languages and logics. My current endeavor is to develop algorithms for type reconstruction, unification, and logic programming in the presence of refinements.
I was advised in my pursuits by Frank Pfenning, patron saint of Logical Frameworks.
Refereed publications:
- Refinement Types for Logical Frameworks and Their Interpretation
as Proof Irrelevance.
William Lovas and Frank Pfenning.
Logical Methods in Computer Science,
Volume 6 (4:5), pp. 1-50, 2010.
( paper: pdf, bibtex ) - Refinement Types as Proof Irrelevance.
William Lovas and Frank Pfenning. 9th International Conference on
Typed Lambda Calculi and Applications (TLCA 2009).
Lecture Notes in Computer Science,
Number 5608, pp. 157-171, 2009.
( paper: pdf, bibtex / talk: pdf ) - 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 2007).
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: Refinement Types for Logical Frameworks.
William Lovas. Sep 2010.
( document: pdf / talk: pdf ) - 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 2010 and Spring of 2011, I TA'd 15-122, Principles of Imperative Computation, a brand new take on the intersection of introductory programming, data structures and algorithms, and computational thinking. (We invented a language for it.) This Summer, I'm teaching a hyper-accelerated version!
In the Fall of 2009, I TA'd 15-317, Constructive Logic, an undergraduate course on really doing logic(s) right.
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 17, 2011 | S (SKK) (SKK) (S (SKK) (SKK)) |