Getting Started in PL Design Research
Download
Report
Transcript Getting Started in PL Design Research
Getting Started in PL
Design Research
Stephanie Weirich
University of Pennsylvania
About Stephanie Weirich
Texan by birth
Pennsylvanian by marriage
Met Steve Zdancewic at grad school (Cornell)
Both PL faculty members at Penn since 2002
Mother of 1.5 girls
grew up in Dallas, attended Rice University
Eleanor Jane Weirich Zdancewic,
Jan 2005
?????, Aug 2007
Research interests
type systems
functional programming
My research
How can we make statically-typed
programming languages more expressive?
Type-directed
Reflect type information structure into data
Express generic algorithms that work for many different data
structures
AspectML, RepLib in Haskell, Type-directed Java
Dependent
Type
Programming: Programs that depend on types
Types: Types that depend on programs
Use types to statically verify program invariants
“Programmable” type systems (conditional relationships)
New language/type system design: PIE
inference
Making it easier to use advanced type systems
Extensions to the Haskell programming language
Where to begin?
Start by building background and experience
Read, Read, Read
Learn by doing: write programs, do proofs
Study textbooks: e.g. Pierce, TAPL
Learn how to evaluate design work
Identify important problems
Work on something that seems cool, even if
you don’t know what the contribution will be
Staring at a blank piece of paper will not produce
a POPL submission.
Where to look for publications
Conferences & Workshops
Journals
POPL & ICFP
PLDI, OOPSLA, ESOP, LICS, PPDP
JFP and TOPLAS
Seminars, web pages
Once you’ve identified the active participants for
your problem
Play with languages
Play around with many different languages
Mature FPLs:
Research FPLs:
Haskell (GHC)
ML (O'Caml, Standard ML)
Scheme (PLT Scheme)
Scala, Omega, ATS, GHC extensions
Why?
Learn by doing
Might find new uses for old types
Might discover connections between features
Learn about constructive logic
Logical foundation for formal models of languages
Books/Lecture notes:
Proof assistants for constructive logic
Barendregt: Lambda Calculi with Types
Pfenning: Computation and Deduction
Sorenson, Urzyczyn: Lectures on the Curry/Howard
Isomorphism
Twelf
Coq
Coq Tutorial at POPL 08 (tentative)
Expressiveness
Build a small interpreter/write small programs
Build a larger implementation/write larger
programs
Port existing programs to new language
Example: Cyclone
Extend existing language with active user
community
Example: GHC
Consistency
Does the design make sense?
Can it be implemented?
Can we prove properties about a formal
model of it?
Type soundness
Decidable type checking
Algorithmic complexity
Aesthetics
Does the design follow general design
principles?
Simplicity
Orthogonality
Mathematical insight
Does the design include a foundational
building block for future languages? Add to
our mathematical vocabulary?
Relevance/Significance
Is there a need for this design?
Example: Concurrency, motivated by new
hardware
Does this design teach us about
programming and program structure?
Example: Monads
What to work on?
What are people talking about now?
What will they be talking about in the next few
years?
What are the important questions?
Another perspective:
Pierce, LICS 2003 invited talk. Types and
Programming Languages: The Next
Generation
Expressive type systems
How do we show that there are no bugs in
linux device drivers/garbage
collectors/embedded systems/etc?
Types for modeling memory management,
state invariants, and running time, eliminating
race conditions, deadlock
Dependent type systems
How can we stop designing all these special
purpose type systems? Can we make the
type system programmable? How can the
user cope with such complicated types?
Indexed types, GADTs, full-spectrum
dependency, PADS, etc.
Program equivalence
How do we show that two programs are the same?
How can we show that program abstractions are
preserved? Even in a multi-lingual system?
Can the design of the language help?
Bisimulation techniques, type abstraction, logical
relations, encryption, security-type systems
Concurrency
What is the right programming model for
concurrent architectures?
Software Transactions?
Deterministic concurrency?
Message-passing?
How do we reason about concurrent
programs?
Does purity help?
How to evaluate language
designs?
Need to know to do good work
Need to know to present that work effectively
Difficult (and sometimes controversial) question
Different axes:
Novelty
Expressiveness
Consistency
Aesthetics
Relevance