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
Fall 2013 office
hours: Tuesdays, 1:30-3:00PM or by
appointment
|
 |
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
|
| |
|