Stephanie Weirich

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 2015 office hours: TBA
Appointment availability

Undergraduate Curriculum: If you have questions regarding Penn's undergraduate programs in Computer Science, send email to .

Quick Links

• My publications (including drafts)
• My github
• Slides from talks and tutorials
• CV and Research summary
• Penn's Programming Languages group (plclub)
  

News and recent activities

• Ron Garcia and I are organizing a mentoring workshop, to be colocated with ICFP 2015
• I will also help judge the Student Research competition at ICFP 2015.
• Submit papers to IFL 2015

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 POPL 2014 paper, as well as papers in MSFP 2012 and PLPV 2012. Also, slides from PLPV 2010 and RDP 2011, give an overview of our work. In 2013 and 2014, I presented a tutorial on designing dependently-typed languages at the Oregon Programming Languages Summer School.
  
  
• Dependently-Typed Haskell: this project works to extend the type system of Haskell with better support for dependently-typed programing. My primary collaborators for this project are Simon Peyton Jones and Dimitrios Vytiniotis at MSR Cambridge, and Penn student Richard Eisenberg.
• Closed Type Families with overlapping equations (POPL 2014) improves the type-level programming capabilities of GHC.
• Down with kinds: adding dependent heterogenous equality to FC (ICFP 2013, with Justin Hsu) extends GHC's core language with support for kind equalities.
  
• Dependently-typed programming with singletons (Haskell Symposium 2012) discusses the singletons library that automatically generates infrastructure for dependently-typed programming.
  
• Giving Haskell a Promotion (TLDI 2012, with José Pedro Magălhaes and Julien Cretin) adds kind polymorphism and datatype promotion to GHC.
• 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.
  
• Type inference for advanced type systems: Advanced type system features, such as first-class polymorphism, impredicative polymorphism and generalized algebraic datatypes, do not interact well with the standard algorithms for type inference in modern typed functional languages, such as ML and Haskell.  Simon Peyton Jones, my students Dimitrios Vytiniotis, Geoffrey Washburn and I have incorporated ideas from Local Type Inference to extend the Glasgow Haskell Compiler with support for these features.
  

Current Ph. D. Students

• Richard A. Eisenberg
  • Dependently-typed Haskell

PhD Graduates


• Geoffrey Washburn, Dec. 2007
• Principia Narcissus: How to avoid being caught by your reflection
• Current employment: LogicBlox
• Dimitrios Vytiniotis, Aug. 2008
• Practical type inference for first-class polymorphism
• Current employment: MSR Cambridge
  
• Chris Casinghino, Dec. 2014
  
  • Combining Proofs and Programs
  • Current employment: Draper Labs
• Brent Yorgey, Dec. 2014
  • Combinatorial Species and Labelled Structures
  • Current employment: Hendrix College
• Vilhelm Sjöberg, May 2015
  • A Dependently Typed Language with Nontermination
  • Current employment: Yale University

Recent Courses

• Spring 15 - Programming Languages and Techniques I (CIS 120)
  
• Fall 14 - Software Foundations (CIS 500)
  
• Spring 14 - Programming Languages and Techniques I (CIS 120)
  
• Fall 13 - Advanced Programming (CIS 552)
  
• Spring 13 - Programming Languages and Techniques I (CIS 120)
  
• Fall 12 - Advanced Programming (CIS 552)
• Spring 12 - Programming Languages and Techniques I (CIS 120)
• Fall 11 - Advanced Programming (CIS 552)
• Spring 11 - Programming Languages and Techniques I (CIS 120)
• Fall 10 - Advanced Topics in Programming Languages (CIS 670)

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