Stephanie Weirich
Associate Professor of Computer and Information Science
School of Engineering
and Applied Science
University of Pennsylvania
Ph.D. (2002) Computer Science
Cornell University
phone:
215.573.2821
fax: 215.898.0587
email: sweirich at cis.upenn.edu
office: 510 Levine Hall
Spring 2013 office
hours: Mondays, 3:30-5PM
|
 |
Quick Links
Research Projects
- TRELLYS: The TRELLYS project seeks to design a
dependently-typed programming language that supports both programming
and theorem proving in the same framework. With Aaron Stump (Iowa
State) and Tim Sheard
(Portland State), we have been discovering what
it means for programs and proofs to interact. See our recent paper submission, as well as papers in MSFP
2012
and PLPV
2012. Also, slides from PLPV
2010 and RDP 2011, give an
overview of our work.
- Dependently-Typed Haskell:
Working with Simon
Peyton Jones and Dimitrios
Vytiniotis at MSR Cambridge, Penn students Brent Yorgey, Richard
Eisenberg and Justin Hsu and I have been working to extend the type
system of Haskell with better support for dependently-typed programing.
- Type-directed
programming: Defining
functions via type information cuts down
on boilerplate programming as many operations may be defined once, for
all types of data. With my student Brent Yorgey and
collaborator Tim Sheard
(Portland State), I developed Unbound, a Haskell library for
declaratively specifying binding structure and automatically generating
free variable, alpha-equivalence and substitution functions. This
library is built using RepLib, an
expressive library that I developed for generic programming in Haskell.
My student Chris
Casinghino and I explored arity
and type generic programming in Agda, lecture notes
from the
Spring
School on Generic and Indexed Programming provide a gentle
introduction.
- Machine assistance
for programming languages research: Designing and proving
properties about programming languages is hard, but the proofs
themselves are straightforward once you know how to set them up. At the
same time, it is all too easy to miss the one little case that ruins
the
whole "proof". Modern proof assistants, such as Twelf, Coq, and Isabelle
are good at expressing this sort of reasoning, but it is hard to
know where to start. I've been working with the POPLmark team to
issue challenge
problems, organize a workshop,
explore techniques
for
reasoning
about
binding, and develop educational
materials about mechanizing programming language metatheory. Brian
Aydemir developed a library for
programming language metatheory (used in the Penn tutorials) and LNgen, a
tool for automatically proving properties about binding.
Current
Students
PhD Graduates
- Geoffrey
Washburn, Dec.
2007
- Dimitrios
Vytiniotis, Aug. 2008
Recent Courses
Other courses
Contact
Information
postal
mail:
School of Engineering and Applied Science
Department of Computer and Information Science
Levine Hall
3330 Walnut Street
Philadelphia, PA 19104-6389
Advice for
graduate students
Interested in Graduate
Studies at Penn?
CISters
Advice for PhD students in CS
|
| |
|