Conferences and Workshops
[1]

Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers.
InfraGen: Binder Boilerplate at Scale.
In European Symposium on Programming (ESOP), pages 419445,
April 2016.

[2]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed.
Visible Type Application.
In European Symposium on Programming (ESOP), pages 229254,
April 2016.
[ PDF ]

[3]

Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee.
Verified ROSBased Deployment of PlatformIndependent Control
Systems.
In Seventh NASA Formal Methods Symposium, pages 248262,
Pasadena, CA, 2015.
[ PDF ]

[4]

Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence.
In POPL 2015: 42nd ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages, pages 369382, Mumbai, India, January 2015.
[ PDF ]

[5]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe ZeroCost Coercions for Haskell.
In The 19th ACM SIGPLAN International Conference on Functional
Programming, ICFP '14, pages 189202, September 2014.
[ PDF ]

[6]

Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations.
In POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages, pages 671683, San Diego, CA, USA, January 2014.
[ PDF ]

[7]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language.
In POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages, pages 3345, San Diego, CA, USA, 2014.
[ PDF ]

[8]

Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with explicit kind equality.
In Proceedings of The 18th ACM SIGPLAN International Conference
on Functional Programming, ICFP '13, pages 275286, Boston, MA, September
2013.
[ PDF ]

[9]

Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam,
Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie
Weirich, and Insup Lee.
Towards synthesis of platformaware attackresilient control
systems: extended abstract.
In HiCoNS '13: Proceedings of the 2nd ACM international
conference on High confidence networked systems, pages 7576, New York, NY,
USA, 2013.

[10]

Richard A. Eisenberg and Stephanie Weirich.
Dependently typed programming with singletons.
In Haskell Symposium, pages 117130, Copenhagen, Denmark,
September 2012.
[ PDF ]

[11]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
StepIndexed Normalization for a Language with General
Recursion.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP '12), pages 2539, 2012.
[ PDF ]

[12]

Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley
D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie
Weirich.
Irrelevance, Heterogenous Equality, and Callbyvalue Dependent
Type Systems.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP '12), pages 112162, 2012.
[ PDF ]

[13]

Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard,
Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and
Ki Yung Ahn.
Equational Reasoning about Programs with General Recursion and
Callbyvalue Semantics.
In Sixth ACM SIGPLAN Workshop Programming Languages meets
Program Verification (PLPV '12), pages 1526, 2012.
[ PDF ]

[14]

Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
Dimitrios Vytiniotis, and José Pedro Magalhaes.
Giving Haskell A Promotion.
In Seventh ACM SIGPLAN Workshop on Types in Language Design and
Implementation (TLDI '12), pages 5366, 2012.
[ PDF ]

[15]

Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.
Binders Unbound.
In Proceeding of the 16th ACM SIGPLAN International Conference
on Functional Programming, ICFP '11, pages 333345, New York, NY, USA,
2011.
[ PDF ]
Keywords: generic programming, haskell, name binding, patterns

[16]

Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Typelevel Computation.
In POPL 11: 38th ACM SIGACTSIGPLAN Symposium on Principles of
Programming Languages, January 2628, 2011. Austin, TX, USA., pages
227240, January 2011.
[ PDF ]
Modular languages support generative type abstraction,
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this wellestablished
feature is in tension with the nonparametric features
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and nonparametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for typelevel computation, but the same
issues should arise whenever generativity and nonparametric features
are combined.

[17]

Tim Sheard, Aaron Stump, and Stephanie Weirich.
LanguageBased Verification Will Change The World.
In 2010 FSE/SDP Workshop on the Future of Software Engineering
Research, pages 343348, November 2010.
Position paper.
[ PDF ]

[18]

Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich.
Termination Casts: A Flexible Approach to Termination with
General Recursion.
In Workshop on Partiality and Recursion in Interactive Theorem
Provers, pages 7693, Edinburgh, Scotland, July 2010.
[ PDF ]
This paper proposes a typeandeffect system that
distinguishes terminating terms and total functions from possibly
diverging terms and partial functions, for a lambda calculus with
general recursion and equality types. The central idea is to include
a primitive typeform “Terminates t”, expressing that term t is
terminating; and then allow terms t to be coerced from possibly
diverging to total, using a proof of Terminates t. We call such
coercions termination casts, and show how to implement
terminating recursion using them. For the metatheory of the system,
we describe a translation from this system to a logical theory of
termination for general recursive, simply typed functions. Every
typing judgment of this system is translated to a theorem expressing the
appropriate termination property of the computational part of the
term.

[19]

Michael Greenberg, Benjamin Pierce, and Stephanie Weirich.
Contracts Made Manifest.
In 37th ACM SIGACTSIGPLAN Symposium on Principles of
Programming Languages (POPL), pages 353364, Madrid, Spain, January 2010.
[ PDF ]
Since Findler and Felleisen introduced higherorder contracts, many
variants have been proposed. Broadly, these fall into two groups:
some follow Findler and Felleisen in using latent contracts, purely
dynamic checks that are transparent to the type system; others use
manifest contracts, where refinement types record the most recent
check that has been applied to each value. These two approaches are
commonly assumed to be equivalentdifferent ways of implementing the
same idea, one retaining a simple type system, and the other providing
more static information. Our goal is to formalize and clarify this
folklore understanding.
Our work extends that of Gronski and Flanagan, who defined a latent
calculus lambdac and a manifest calculus lambdah, gave a translation
phi from lambdac to lambdah, and proved that, if a lambdac term
reduces to a constant, then so does its phiimage. We enrich their
account with a translation psi from lambdah to lambdac and prove an
analogous theorem.
We then generalize the whole framework to dependent contracts, whose
predicates can mention free variables. This extension is both
pragmatically crucial, supporting a much more interesting range of
contracts, and theoretically challenging. We define dependent
versions of lambdah and two dialects (“lax” and “picky”) of
lambdac, establish type soundnessa substantial result in itself,
for lambdahand extend phi and psi accordingly. Surprisingly, the
intuition that the latent and manifest systems are equivalent now
breaks down: the extended translations preserve behavior in one
direction but, in the other, sometimes yield terms that blame more.

[20]

Limin Jia, Jianzhou Zhao, Vilhem Sjöberg, and Stephanie Weirich.
Dependent types and Program Equivalence.
In 37th ACM SIGACTSIGPLAN Symposium on Principles of
Programming Languages (POPL), pages 275286, Madrid, Spain, January 2010.
[ PDF ]
The definition of type equivalence is one of the most important design
issues for any typed language. In dependentlytyped languages, because
terms appear in types, this definition must rely on a definition of
term equivalence. In that case, decidability of type checking requires
decidability for the term equivalence relation.
Almost all dependentlytyped languages require this relation to be
decidable. Some, such as Coq, Epigram or Agda, do so by employing
analyses to force all programs to terminate. Conversely, others, such
as DML, ATS, Omega, or Haskell, allow nonterminating computation, but
do not allow those terms to appear in types. Instead, they identify a
terminating index language and use singleton types to connect indices
to computation. In both cases, decidable type checking comes at a
cost, in terms of complexity and expressiveness.
Conversely, the benefits to be gained by decidable type checking are
modest. Termination analyses allow dependently typed programs to
verify total correctness properties. However, decidable type checking
is not a prerequisite for type safety. Furthermore, decidability does
not imply tractability. A decidable approximation of program
equivalence may not be useful in practice.
Therefore, we take a different approach: instead of a fixed notion for
term equi valence, we parameterize our type system with an abstract
relation that is not n ecessarily decidable. We then design a novel
set of typing rules that require on ly weak properties of this
abstract relation in the proof of the preservation an d progress
lemmas. This design provides flexibility: we compare valid instantiat
ions of term equivalence which range from betaequivalence, to
contextual equiva lence, to some exotic equivalences.

[21]

Stephanie Weirich and Chris Casinghino.
Aritygeneric typegeneric programming.
In ACM SIGPLAN Workshop on Programming Languages Meets Program
Verification (PLPV), pages 1526, January 2010.
[ PDF ]

[22]

Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and
Steve Zdancewic.
Reactive Noninterference.
In 16th ACM Conference on Computer and Communications Security,
pages 7990, November 2009.
[ PDF ]
Many programs operate reactivelypatiently waiting for user input, running
for a while producing output, and eventually returning to a state where they
are ready to accept another input (or occasionally diverging). When a
reactive program communicates with multiple parties, we would like to be
sure that it can be given secret information by one without leaking it to
others.
Motivated by web browsers and clientside web applications,
we explore definitions of noninterference for reactive programs and
identify two of special interestone corresponding to
terminationinsensitive noninterference for a simple sequential language,
the other to terminationsensitive noninterference. We focus on the former
and develop a proof technique for showing that program behaviors are secure
according to this definition. To demonstrate the viability of the approach,
we define a simple reactive language with an informationflow type system
and apply our proof technique to show that welltyped programs are secure.

[23]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
FPH: Firstclass polymorphism for Haskell.
In ICFP 2008: The 13th ACM SIGPLAN International Conference on
Functional Programming, pages 295306, Victoria, BC, Canada, September
2008.
[ PDF ]
Languages supporting polymorphism typically have adhoc restrictions
on where polymorphic types may occur. Supporting “firstclass” polymorphism,
by lifting those restrictions, is obviously desirable, but it is hard
to achieve this without sacrificing type inference. We present a new
type system for higherrank and impredicative polymorphism that improves
on earlier proposals: it is an extension of DamasMilner;
it relies only on System F types; it has a simple, declarative specification;
it is robust to program transformations; and it enjoys a complete and decidable
type inference algorithm.

[24]

Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich.
Engineering Formal Metatheory.
In ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages (POPL), pages 315, January 2008.
[ Project
PDF ]
Machinechecked proofs of properties of programming languages have become a
critical need, both for increased confidence in large and complex designs
and as a foundation for technologies such as proofcarrying code. However,
constructing these proofs remains a black art, involving many choices in the
formulation of definitions and theorems that make a huge cumulative
difference in the difficulty of carrying out large formal developments. The
representation and manipulation of terms with variable binding is a
key issue.
We propose a novel style for formalizing metatheory, combining
locally nameless representation of terms and
cofinite quantification of free variable names in inductive
definitions of relations on terms (typing, reduction, ...). The
key technical insight is that our use of cofinite quantification
obviates the need for reasoning about equivariance (the fact that free
names can be renamed in derivations); in particular, the structural
induction principles of relations defined using cofinite
quantification are strong enough for metatheoretic reasoning, and
need not be explicitly strengthened.
Strong inversion principles follow (automatically, in Coq) from the
induction principles. Although many of the underlying ingredients of
our technique have been used before, their combination here yields a
significant improvement over existing methodology, leading to
developments that are faithful to informal practice, yet require no
external tool support and little infrastructure within the proof
assistant.
We have carried out several large developments in this style using the Coq
proof assistant and have made them publicly available. Our developments
include type soundness for and ML (with references, exceptions,
datatypes, recursion and patterns) and subject reduction for the Calculus of
Constructions. Not only do these developments demonstrate the
comprehensiveness of our approach; they have also been optimized for clarity
and robustness, making them good templates for future extension.

[25]

Dimitrios Vytiniotis and Stephanie Weirich.
Dependent types: Easy as PIE.
In Marco T. Morazán and Henrik Nilsson, editors, Draft
Proceedings of the 8th Symposium on Trends in Functional Programming, pages
XVII1XVII15. Dept. of Math and Computer Science, Seton Hall
University, April 2007.
TRSHUCS2007041.
[ PDF ]

[26]

Dimitrios Vytiniotis and Stephanie Weirich.
Free theorems and runtime type representations.
In Mathematical Foundations of Programming Semantics (MFPS
XXIII), pages 357373, New Orleans, LA, USA, April 2007.
[ PDF
PS ]
Reynolds' abstraction theorem, often referred to
as the parametricity theorem, can be used to derive properties about
functional programs solely from their types. Unfortunately, in the
presence of runtime type analysis, the abstraction properties of
polymorphic programs are no longer valid. However, runtime type
analysis can be implemented with termlevel representations of
types, as in the language of Crary et
al., where case analysis on
these runtime representations introduces type refinement. In this
paper, we show that representationbased analysis is consistent with
type abstraction by extending the abstraction theorem to such a
language. We also discuss the “free theorems” that result. This
work provides a foundation for the more general problem of extending
the abstraction theorem to languages with generalized algebraic
datatypes.

[27]

Stephanie Weirich.
RepLib: A library for derivable type classes.
In Haskell Workshop, pages 112, Portland, OR, USA, September
2006.
[ Project
PDF ]
Some type class instances can be automatically derived from the
structure of types. As a result, the Haskell language includes the
"deriving" mechanism to automatic generates such instances for a
small number of builtin type classes. In this paper, we present
RepLib, a GHC library that enables a similar mechanism for arbitrary
type classes. Users of RepLib can define the relationship between
the structure of a datatype and the associated instance declaration
by a normal Haskell functions that patternmatches a representation
types. Furthermore, operations defined in this manner are
extensibleinstances for specific types not defined by type
structure may also be incorporated. Finally, this library also
supports the definition of operations defined by parameterized
types.

[28]

Geoffrey Washburn and Stephanie Weirich.
Good Advice for Typedirected Programming: Aspectoriented
Programming and Extensible Generic Functions.
In Workshop on Generic Programming (WGP), pages 3344,
Portland, OR, USA, September 2006.
[ Project
PDF ]
Typedirected programming is an important idiom for software design.
In typedirected programming the behavior of programs is guided by the
type structure of data. It makes it possible to implement many sorts
of operations, such as serialization, traversals, and queries, only
once and without needing to continually revise their implementation as
new data types are defined.
Typedirected programming is the basis for recent research into
"scrapping" tedious boilerplate code that arises in functional
programming with algebraic data types. This research has primarily
focused on writing typedirected functions that are closed to
extension. However, Lämmel and Peyton Jones recently developed a
technique for writing openly extensible typedirected functions in
Haskell by making clever use of type classes. Unfortunately, this
technique has a number of limitations.
We present an alternate approach to writing openly extensible
typedirected functions by using the aspectoriented programming
features provided by the language AspectML. Our solution not only
avoids the limitations present in Lämmel and Peyton Jones technique,
but also allows typedirected functions to be extended at any time
with cases for types that were not even known at compiletime. This
capability is critical to writing programs that make use of dynamic
loading or runtime type generativity.

[29]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Boxy type inference for higherrank types and impredicativity.
In International Conference on Functional Programming (ICFP),
pages 251262, Portland, OR, USA, September 2006.
[ Project
PDF ]
Languages with rich type systems are beginning to
employ a blend of type inference and type
checking, so that the type inference engine is
guided by programmersupplied type annotations. In
this paper we show, for the first time, how to combine
the virtues of two wellestablished ideas:
unificationbased inference, and bidirectional
propagation of type annotations. The result is a type
system that conservatively extends HindleyMilner, and
yet supports both higherrank types and
impredicativity.

[30]

Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn.
Simple unificationbased type inference for GADTs.
In International Conference on Functional Programming (ICFP),
pages 5061, Portland, OR, USA, September 2006.
[ PDF ]
Generalized algebraic data types (GADTs), sometimes known as “guarded
recursive data types” or “firstclass phantom
types”, are a simple but powerful generalization of
the data types of Haskell and ML. Recent works have
given compelling examples of the utility of GADTs,
although type inference is known to be difficult. Our
contribution is to show how to exploit
programmersupplied type annotations to make the type
inference task almost embarrassingly easy. Our main
technical innovation is wobbly types, which express in
a declarative way the uncertainty caused by the
incremental nature of typical typeinference
algorithms.

[31]

Brian Aydemir, Aaron Bohannon, and Stephanie Weirich.
Nominal Reasoning Techniques in Coq.
In International Workshop on Logical Frameworks and
MetaLanguages:Theory and Practice (LFMTP), pages 6069, Seattle, WA, USA,
August 2006.
[ Project
PDF ]
We explore an axiomatized nominal approach to variable binding in Coq,
using an untyped lambdacalculus as our test case. In our nominal
approach, alphaequality of lambda terms coincides with Coq's builtin
equality. Our axiomatization includes a nominal induction principle and
functions for calculating free variables and substitution. These axioms
are collected in a module signature and proved sound
using locally nameless terms as the underlying
representation. Our experiences so far suggests that it is feasible to
work from such axiomatized theories in Coq and that the nominal style of
variable binding corresponds closely with paper proofs. We are currently
working on proving the soundness of a primitive recursion combinator
and developing a method of generating these axioms and their proof of
soundness from a grammar describing the syntax of terms and binding.

[32]

Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic.
It is Time to Mechanize Programming Language Metatheory.
In Verified Software: Theories, Tools, Experiments (VS:TTE),
pages 2630, Zürich, Switzerland, October 2005.
[ Project
PDF ]
How close are we to a world in which mechanically verified software is
commonplace? A world in which theorem proving technology is used
routinely by both software developers and programming
language researchers alike? One crucial step towards achieving these
goals is mechanized reasoning about language metatheory. The time has
come to bring together the theorem proving and programming language
communities to address this problem. We have proposed the POPLMark
challenge as a concrete set of benchmarks intended both for measuring
progress in this area and for stimulating discussion and
collaboration. Our goal is to push the boundaries of existing
technology to the point where we can achieve mechanized metatheory for
the masses.

[33]

Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
PolyAML: A polymorphic aspectoriented functional programmming
language.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), pages 306319, Tallinn, Estonia, September 2005.
[ Project
PDF
PS ]
This paper defines PolyAML, a typed functional and aspectoriented
programming language. The main contribution of PolyAML is in the
seamless integration of polymorphism, runtime type analysis and
aspectoriented programming language features. In particular, PolyAML
allows programmers to define typesafe polymorphic advice using pointcuts
constructed from a collection of polymorphic join points. PolyAML
also comes equipped with a type inference algorithm that conservatively
extends HindleyMilner type inference. In order to support firstclass
polymorphic pointcut designators, a crucial feature for developing
aspectoriented profiling or logging libraries, the algorithm blends the
conventional HindleyMilner type inference algorithm with a simple form
of local type inference.
We give our language operational meaning via a typedirected
translation into an expressive typesafe intermediate language. Many
complexities of the source language are eliminated in this
translation, leading to a modular specification of its semantics. One
of the novelties of the intermediate language is the definition of
polymorphic labels for marking controlflow points. These labels are
organized in a tree structure such that a parent in the tree serves as
a representative for the collection of all its children. Type safety
requires that the type of each child is a generic instance of the type
of the polymorphic parent. Similarly, when a set of labels is
assembled as a pointcut, the type of each label is an instance of the
type of the pointcut.

[34]

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster,
Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn,
Stephanie Weirich, and Steve Zdancewic.
Mechanized Metatheory for the Masses: The POPLmark Challenge.
In The 18th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs), pages 5065, Oxford, UK, August 2005.
[ Project
PDF
PS ]
How close are we to a world where every paper on
programming languages is accompanied by an electronic appendix with
machinechecked proofs?
We propose a concrete set of benchmarks for measuring progress in this
area. Based on the metatheory of System Fsub, a typed
lambdacalculus with secondorder polymorphism, subtyping, and
records, these benchmarks embody many aspects of programming languages
that are challenging to formalize: variable binding at both the term
and type levels, syntactic forms with variable numbers of components
(including binders), and proofs demanding complex induction
principles. We hope that these benchmarks will help clarify the
current state of the art, provide a basis for comparing competing
technologies, and motivate further research.

[35]

Geoffrey Washburn and Stephanie Weirich.
Generalizing Parametricity Using Information Flow.
In Twentieth Annual IEEE Symposium on. Logic in Computer Science
(LICS 2005), pages 6271, Chicago, IL, USA, June 2005.
[ Project
PDF
PS ]
Runtime type analysis allows programmers to easily and
concisely define many operations based upon type structure, such as
serialization, iterators, and structural equality. However, when
types can be inspected at run time, nothing is secret. A module
writer cannot use type abstraction to hide implementation details from
clients: those clients can use type analysis to determine the
structure of these supposedly “abstract” data types. Furthermore,
access control mechanisms do not help in isolating the implementation
of abstract datatypes from their clients. Buggy or malicious
authorized modules may simply leak type information to unauthorized
clients, so module implementors cannot reliably tell which parts of a
program rely on their type definitions and which parts do not.
Currently, module implementors rely on parametric polymorphism to
provide guarantees about the use of their abstract datatypes.
Standard type parametricity does not hold for a language with runtime
type analysis, but in this paper we show how to generalize the
statement of parametricity so that it does hold in the presence of
type analysis and still encompasses the integrity and confidentiality
policies that are normally derived from parametricity. The key is to
augment the type system with annotations about information flow.
Because the type system tracks the flow of dynamic type information,
the implementor of an abstract data type can easily see what parts of
the program depend on the implementation of a given type.

[36]

Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich.
An Open and Shut Typecase.
In ACM SIGPLAN Workshop on Types in Language Design and
Implementation, pages 1324, Long Beach, CA, USA, January 2005.
[ PS ]
Two different ways of defining adhoc polymorphic operations commonly
occur in programming languages. With the first form polymorphic
operations are defined inductively on the structure of types while
with the second form polymorphic operations are defined for specific
sets of types.
In intensional type analysis operations are defined by induction on
the structure of types. Therefore no new cases are necessary for
userdefined types, because these types are equivalent to their
underlying structure. However, intensional type analysis is
“closed” to extension, as the behavior of the operations cannot be
differentiated for the new types, thus destroying the distinctions
that these types are designed to express.
Haskell type classes on the other hand define polymorphic operations
for sets of types. Operations defined by class instances are
considered “open”the programmer can add instances for new types
without modifying existing code. However, the operations must be
extended with specialized code for each new type, and it may be
tedious or even impossible to add extensions that apply to a large
universe of new types.
Both approaches have their benefits, so it is important to let
programmers decide which is most appropriate for their needs. In this
paper, we define a language that supports both forms of adhoc
polymorphism, using the same basic constructs.

[37]

Stephanie Weirich and Liang Huang.
A Design for TypeDirected Java.
In Viviana Bono, editor, Workshop on ObjectOriented
Developments (WOOD), ENTCS, pages 117136, August 2004.
[ Project
PDF
PS ]
Typedirected programming is an important and widely used
paradigm in the design of software. With this form of programming,
an application may analyze type information to determine its
behavior. By analyzing the structure of data, many operations, such
as serialization, cloning, adaptors and iterators may be defined
once, for all types of data. That way, as the program evolves, these
operations need not be updatedthey will automatically adapt to
new data forms. Otherwise, each of these operations must be
individually redefined for each type of data, forcing programmers to
revisit the same program logic many times during a program's
lifetime.
The Java language supports type directed programming with the
instanceof operator and the Java Reflection API. These
mechanisms allow Java programs to depend on the name and structure
of the runtime classes of objects. However, the Java mechanisms
for typedirected programming are difficult to use. They also do not
integrate well with generics, an important new feature of the Java
language.
In this paper, we describe the design of several expressive new
mechanisms for typedirected programming in Java, and show that
these mechanisms are sound when included in a language similar to
Featherweight Java. Basically, these new mechanisms patternmatch
the name and structure of the type parameters of generic code,
instead of the runtime classes of objects. Therefore, they
naturally integrate with generics and provide strong guarantees
about program correctness. As these mechanisms are based on pattern
matching, they naturally and succinctly express many operations that
depend on type information. Finally, they provide programmers with
some degree of protection for their abstractions. Whereas
instanceof and reflection can determine the exact runtime type
of an object, our mechanisms allow any supertype to be supplied for
analysis, hiding its precise structure.

[38]

Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higherorder Abstract Syntax with
Parametric Polymorphism.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), pages 249262, Uppsala, Sweden, August 2003.
[ PDF
PS ]
Higherorder abstract syntax is a simple technique for
implementing languages with functional programming. Object variables
and binders are implemented by variables and binders in the host
language. By using this technique, one can avoid implementing common
and tricky routines dealing with variables, such as captureavoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higherorder abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how firstclass polymorphism can be used to
guarantee the parametricity of functions embedded in higherorder
abstract syntax. With this restriction, we implement a library of
iteration operators over datastructures containing functionals. From
this implementation, we derive “fusion laws” that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Schuermann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System Fomega.
This encoding can serve as a starting point for reasoning about
higherorder structures in polymorphic languages.

[39]

Stephanie Weirich.
HigherOrder Intensional Type Analysis.
In Daniel Le Métayer, editor, 11th European Symposium on
Programming (ESOP), pages 98114, Grenoble, France, April 2002.
[ PDF
PS ]
Intensional type analysis provides the ability to
analyze abstracted types at run time. In this paper, we extend
that ability to higherorder and kindpolymorphic type
constructors. The resulting language is elegant and expressive:
we show through examples how it extends the repertoire of
polytypic functions that may be defined.

[40]

Stephanie Weirich.
Encoding Intensional Type Analysis.
In D. Sands, editor, 10th European Symposium on Programming
(ESOP), pages 92106, Genova, Italy, April 2001.
[ PDF
PS
http ]
Languages for intensional type analysis permit adhoc
polymorphism, or runtime analysis of types. However, such
languages require complex, specialized constructs to support this
operation, which hinder optimization and complicate the
metatheory of these languages. In this paper, we observe that
such specialized operators need not be intrinsic to the language,
and in fact, their operation may be simulated through standard
encodings of iteration in the polymorphic lambda
calculus. Therefore, we may more easily add intensional analysis
operators to complicated languages via a translation semantics,
instead of through language extension.

[41]

Stephanie Weirich.
TypeSafe Cast: Functional Pearl.
In Proceedings of the fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 5867, Montreal, Canada,
September 2000.
[ PDF
PS ]
In a language with nonparametric or adhoc
polymorphism, it is possible to determine the identity of a type
variable at run time. With this facility, we can write a function
to convert a term from one abstract type to another, if the two
hidden types are identical. However, the naive implementation of
this function requires that the term be destructed and rebuilt. In
this paper, we show how to eliminate this overhead using
higherorder type abstraction. We demonstrate this solution in two
frameworks for adhoc polymorphism: intensional type analysis and
type classes.

[42]

Karl Crary and Stephanie Weirich.
Resource Bound Certification.
In The TwentySeventh ACM SIGPLANSIGACT Symposium on
Principles of Programming Languages (POPL), pages 184198, Boston, MA, USA,
January 2000.
[ PDF
PS ]
Various code certification systems allow the
certification and static verification of a variety of important
safety properties such as memory safety and controlflow
safety. These systems provide valuable tools for verifying that
untrusted and potentially malicious code is safe before execution.
However, one important safety property that is not usually
included is that programs adhere to specific bounds on resource
consumption, such as running time.
We present a decidable type system capable of specifying and
certifying bounds on resource consumption. Our system makes two
advances over previous resource bound certification systems, both
of which are necessary for a practical system: we allow the
execution time of programs and their subroutines to vary,
depending on their arguments, and we provide a fully automatic
compiler generating certified executables from sourcelevel
programs. The principal device in our approach is a strategy for
simulating dependent types using sum and inductive kinds.

[43]

Karl Crary and Stephanie Weirich.
Flexible Type Analysis.
In Proceedings of the fourth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 233248, Paris, France,
September 1999.
[ PDF
PS ]
Runtime type dispatch enables a variety of advanced
optimization techniques for polymorphic languages, including
tagfree garbage collection, unboxed function arguments, and
flattened data structures. However, modern typepreserving
compilers transform types between stages of compilation, making
type dispatch prohibitively complex at low levels of typed
compilation. It is crucial therefore for type analysis at these
low levels to refer to the types of previous
stages. Unfortunately, no current intermediate language supports
this facility.
To fill this gap, we present the language LX, which provides a
rich language of type constructors supporting type analysis
(possibly of previousstage types) as a programming idiom. This
language is quite flexible, supporting a variety of other
applications such as analysis of quantified types, analysis with
incomplete type information, and type classes. We also show that
LX is compatible with a typeerasure semantics.

[44]

Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick
Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.
TALx86: A Realistic Typed Assembly Language.
In Second ACM SIGPLAN Workshop on Compiler Support for
System Software, pages 2535, Atlanta, GA, USA, May 1999.
Published as INRIA research report number 0228, March 1999.
[ PDF
PS ]
The goal of typed assembly language (TAL) is to provide
a lowlevel, statically typed target language that is better
suited than Java bytecodes for supporting a wide variety of
source languages and a number of important optimizations. In
previous work, we formalized idealized versions of TAL and proved
important safety properties about them. In this paper, we present
our progress in defining and implementing a realistic typed
assembly language called TALx86. The TALx86 instructions comprise
a relatively complete fragment of the Intel IA32 (32bit 80x86
flat model) assembly language and are thus executable on
processors such as the Intel Pentium. The type system for the
language incorporates a number of advanced features necessary for
safely compiling large programs to good code.
To motivate the design of the type system, we demonstrate how
various highlevel language features are compiled to TALx86. For
this purpose, we present a typesafe Clike language called
Popcorn.

[45]

Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics.
In Proceedings of the third ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 301313, Baltimore, MD,
USA, September 1998.
[ PDF
PS ]
Intensional polymorphism, the ability to dispatch to
different routines based on types at run time, enables a variety of
advanced implementation techniques for polymorphic languages,
including tagfree garbage collection, unboxed function arguments,
polymorphic marshalling, and flattened data structures. To date,
languages that support intensional polymorphism have required a
typepassing (as opposed to typeerasure) interpretation where types
are constructed and passed to polymorphic functions at run
time. Unfortunately, typepassing suffers from a number of
drawbacks; it requires duplication of constructs at the term and
type levels, it prevents abstraction, and it severely complicates
polymorphic closure conversion. We present a typetheoretic
framework that supports intensional polymorphism, but avoids many of
the disadvantages of type passing. In our approach, runtime type
information is represented by ordinary terms. This avoids the
duplication problem, allows us to recover abstraction, and avoids
complications with closure conversion. In addition, our type system
provides another improvement in expressiveness; it allows unknown
types to be refined in place thereby avoiding certain
betaexpansions required by other frameworks.

[46]

Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and
Matthias Felleisen.
Catching Bugs in the Web of Program Invariants.
In ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI), pages 2332, 1996.
[ PDF
PS ]
MrSpidey is a userfriendly, interactive static
debugger for Scheme. A static debugger supplements the standard
debugger by analyzing the program and pinpointing those program
operations tha may cause runtime errors suce as dereferencing
the null pointer or applying nonfunctions. The program analysis
of MrSpidey computes value set descriptions for each term in the
program and constructs a value flow graph connecting the set
descriptions. Using the set descriptions, MrSpidey can identify
and highlight potentially erroneous program operations, whose
cause the programmer can the explore by selectively exposing
portions of the value flow graph.


Journal Articles
[1]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe zerocost coercions for Haskell.
Journal of Functional Programming, 26, 007 2016.
[ DOI
PDF
http ]
AbstractGenerative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a runtime representation with some base type. We present a new mechanism that allows for zerocost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

[2]

Garrin Kimmel, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie
Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathin Collins, and Ki Yunh
Anh.
Equational reasoning about programs with general recursion and
callbyvalue semantics.
Progress in Informatics, (10):1948, March 2013.
[ http ]

[3]

Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts made manifest.
Journal of Functional Programming, 22(3):225274, May 2012.

[4]

Dimitrios Vytiniotis and Stephanie Weirich.
Parametricity, Type Equality and Higherorder Polymorphism.
Journal of Functional Programming, 20(2):175210, March 2010.
[ PDF ]
Propositions that express type equality are a frequent ingredient of
modern functional programmingthey can encode generic
functions, dynamic types, and GADTs. Via the CurryHoward
correspondence, these propositions are ordinary types
inhabited by proof terms, computed using runtime type
representations. In this paper we show that two examples of type
equality propositions actually do reflect type equality; they are
only inhabited when their arguments are equal and their proofs are
unique (up to contextual equivalence.) We show this result in the
context of a strongly normalizing language with higherorder
polymorphism and primitive recursion over runtime type
representations by proving Reynolds's abstraction theorem. We then
use this theorem to derive “free” theorems about equality types.

[5]

Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
AspectML: A Polymorphic Aspectoriented Functional Programming
Language.
ACM Transactions on Programming Languages, 30(3):160, May
2008.
[ Project
PDF ]
This paper defines Aspectml, a typed functional, aspectoriented
programming language. The main contribution of Aspectml is the
seamless integration of polymorphism, runtime type analysis
and aspectoriented programming language features. In particular,
Aspectml allows programmers to define typesafe polymorphic advice
using pointcuts constructed from a collection of polymorphic join
points. Aspectml also comes equipped with a type inference algorithm
that conservatively extends HindleyMilner type inference. To support
firstclass polymorphic pointcut designators, a crucial feature for
developing aspectoriented profiling or logging libraries, the
algorithm blends the conventional HindleyMilner type inference
algorithm with a simple form of local type inference.
We give our language operational meaning via a typedirected
translation into an expressive typesafe intermediate language. Many
complexities of the source language are eliminated in this
translation, leading to a modular specification of its semantics. One
of the novelties of the intermediate language is the definition of
polymorphic labels for marking controlflow points. These labels are
organized in a tree structure such that a parent in the tree serves as
a representative for all of its children. Type safety requires that
the type of each child is less polymorphic than its parent
type. Similarly, when a set of labels is assembled as a pointcut, the
type of each label is an instance of the type of the pointcut.

[6]

Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higherorder Abstract Syntax with
Parametric Polymorphism.
Journal of Functional Programming, 18(1):87140, January 2008.
[ PDF ]
Higherorder abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as captureavoiding
substitution. However, despite the advantages this technique provides,
it is not commonly used because it is difficult to write sound
elimination forms (such as folds or catamorphisms) for
higherorder abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how firstclass polymorphism can be used to
guarantee the parametricity of functions embedded in higherorder
abstract syntax. With this restriction, we implement a library of
iteration operators over datastructures containing functionals. From
this implementation, we derive fusion laws that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Schürmann, Despeyroux and Pfenning method of enforcing parametricity
through modal types. We do so by using this library to give a sound
and complete encoding of their calculus into System Fomega. This
encoding can serve as a starting point for reasoning about
higherorder structures in polymorphic languages.

[7]

Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitraryrank types.
Journal of Functional Programming, 17(1):182, January 2007.
[ Project
PDF ]
Haskell's popularity has driven the need for ever more expressive type
system features, most of which threaten the decidability and
practicality of DamasMilner type inference. One such feature is the
ability to write functions with higherrank types  that is,
functions that take polymorphic functions as their arguments.
Complete type inference is known to be undecidable for higherrank
(impredicative) type systems, but in practice programmers are more
than willing to add type annotations to guide the type inference
engine, and to document their code. However, the choice of just what
annotations are required, and what changes are required in the type
system and its inference algorithm, has been an ongoing topic of
research.
We take as our starting point a lambdacalculus proposed by Odersky
and Laufer. Their system supports arbitraryrank polymorphism through
the exploitation of type annotations on lambdabound arguments and
arbitrary subterms. Though elegant, and more convenient than some
other proposals, Odersky and Laufer's system requires many
annotations. We show how to use local type inference (invented by
Pierce and Turner) to greatly reduce the annotation burden, to the
point where higherrank types become eminently usable.
Higherrank types have a very modest impact on type inference. We
substantiate this claim in a very concrete way, by presenting a
complete typeinference engine, written in Haskell, for a traditional
DamasMilner type system, and then showing how to extend it for
higherrank types. We write the typeinference engine using a monadic
framework: it turns out to be a particularly compelling example of
monads in action.
The paper is long, but is strongly tutorial in style.

[8]

Stephanie Weirich.
TypeSafe Runtime Polytypic Programming.
Journal of Functional Programming, 16(10):681710, November
2006.
[ PDF ]
Polytypic programming is a way of defining typeindexed
operations, such as map, fold and zip, based on type information.
Runtime polytypic programming allows that type information to
be dynamically computedthis support is essential in modern
programming languages that support separate compilation, firstclass
type abstraction, or polymorphic recursion.
However, in previous work we defined runtime polytypic programming
with a typepassing semantics. Although it is natural to define
polytypic programs as operating over firstclass types, such a
semantics suffers from a number of drawbacks. This paper describes
how to recast that work in a typeerasure semantics, where terms
represent type information in a safe manner. The resulting language
is simple and easy to implementwe present a prototype
implementation of the necessary machinery as a small Haskell
library.

[9]

Stephanie Weirich.
TypeSafe Cast.
Journal of Functional Programming, 14(6):681695, November
2004.
[ PDF ]
Comparing two types for equality is an essential ingredient for an
implementation of dynamic types. Once equality has been established,
it is safe to cast a value from one type to another. In a language
with runtime type analysis, implementing such a procedure is fairly
straightforward. Unfortunately, this naive implementation destructs
and rebuilds the argument while iterating over its type structure.
However, by using higherorder polymorphism, a casting function can
treat its argument parametrically. We demonstrate this solution in
two frameworks for adhoc polymorphism: intensional type analysis
and Haskell type classes.

[10]

Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics.
Journal of Functional Programming, 12(6):567600, November
2002.
[ PDF ]
Intensional polymorphism, the ability to dispatch to
different routines based on types at run time, enables a variety
of advanced implementation techniques for polymorphic languages,
including tagfree garbage collection, unboxed function
arguments, polymorphic marshalling, and flattened data
structures. To date, languages that support intensional
polymorphism have required a typepassing (as opposed to
typeerasure) interpretation where types are constructed and
passed to polymorphic functions at run time. Unfortunately,
typepassing suffers from a number of drawbacks; it requires
duplication of constructs at the term and type levels, it
prevents abstraction, and it severely complicates polymorphic
closure conversion. We present a typetheoretic framework that
supports intensional polymorphism, but avoids many of the
disadvantages of type passing. In our approach, runtime type
information is represented by ordinary terms. This avoids the
duplication problem, allows us to recover abstraction, and avoids
complications with closure conversion. In addition, our type
system provides another improvement in expressiveness; it allows
unknown types to be refined in place thereby avoiding certain
betaexpansions required by other frameworks.


Technical Reports
[1]

Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence (Extended Version).
Technical Report MSCIS1410, University of Pennsylvania, October
2014.
[ PDF ]

[2]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe Zerocost Coercions for Haskell (Extended Version).
Technical Report MSCIS1407, Univ. of Pennsylvania, April 2014.
[ PDF ]

[3]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language
(With Technical Appendix).
Technical Report MSCIS1308, University of Pennsylvania, November
2013.
[ PDF ]

[4]

Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations (Extended
version).
Technical Report MSCIS1310, University of Pennsylvania, November
2013.
[ PDF ]

[5]

Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Typelevel Computation (Extended
Version).
Technical report, November 2010.
[ PDF ]
Modular languages support generative type abstraction,
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this wellestablished
feature is in tension with the nonparametric features
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and nonparametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for typelevel computation, but the same
issues should arise whenever generativity and nonparametric features
are combined.

[6]

Brian Aydemir and Stephanie Weirich.
LNgen: Tool Support for Locally Nameless Representations.
Technical Report MSCIS1024, Computer and Information Science,
University of Pennsylvania, June 2010.
[ Project
PDF ]

[7]

Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich.
Termination Casts: A Flexible Approach to Termination with
General Recursion (Technical Appendix).
Technical Report MSCIS1021, University of Pennsylvania Department
of Computer and Information Science, 2010.
[ PDF ]

[8]

Brian Aydemir, Steve Zdancewic, and Stephanie Weirich.
Abstracting Syntax.
Technical Report MSCIS0906, Computer and Information Science,
University of Pennsylvania, March 2009.
[ Project
PDF ]

[9]

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie
Weirich, and Stephan Zdancewic.
Manifest Security.
Technical report, January 2007.
White paper.
[ PDF ]

[10]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Boxy type inference for higherrank types and impredicativity,
Technical Appendix.
Technical Report MSCIS0523, University of Pennsylvania, April
2006.
[ PDF ]

[11]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Simple unificationbased type inference for GADTs, Technical
Appendix.
Technical Report MSCIS0522, University of Pennsylvania, April
2006.
[ PDF ]

[12]

Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitraryrank types (Technical
appendix).
Technical Report MISCIS0514, University of Pennsylvania, July
2005.
[ Project
PDF ]

[13]

Geoffrey Washburn and Stephanie Weirich.
Generalizing Parametricity Using Information Flow (Extended
version).
Technical Report MSCIS0504, Computer and Information Science,
University of Pennsylvania, July 2005.
[ PDF ]
Runtime type analysis allows programmers to easily and
concisely define many operations based upon type structure, such as
serialization, iterators, and structural equality. However, when
types can be inspected at run time, nothing is secret. A module
writer cannot use type abstraction to hide implementation details from
clients: those clients can use type analysis to determine the
structure of these supposedly “abstract” data types. Furthermore,
access control mechanisms do not help in isolating the implementation
of abstract datatypes from their clients. Buggy or malicious
authorized modules may simply leak type information to unauthorized
clients, so module implementors cannot reliably tell which parts of a
program rely on their type definitions and which parts do not.
Currently, module implementors rely on parametric polymorphism to
provide guarantees about the use of their abstract datatypes.
Standard type parametricity does not hold for a language with runtime
type analysis, but in this paper we show how to generalize the
statement of parametricity so that it does hold in the presence of
type analysis and still encompasses the integrity and confidentiality
policies that are normally derived from parametricity. The key is to
augment the type system with annotations about information flow.
Because the type system tracks the flow of dynamic type information,
the implementor of an abstract data type can easily see what parts of
the program depend on the implementation of a given type.

[14]

Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
PolyAML: A Polymorphic AspectOriented Functional Programming
Language (Extended Version).
Technical Report MSCIS0507, University of Pennsylvania, Department
of Computer and Information Science, 2005.
[ PDF ]
This paper defines PolyAML, a typed functional, aspectoriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, runtime type analysis and aspectoriented programming language features. In particular, PolyAML allows programmers to define typesafe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends HindleyMilner type inference. To support firstclass polymorphic pointcut designators, a crucial feature for developing aspectoriented profiling or logging libraries, the algorithm blends the conventional HindleyMilner type inference algorithm with a simple form of local type inference.
We give our language operational meaning via a typedirected translation into an expressive typesafe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking controlflow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.

[15]

Dan S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
Analyzing Polymorphic Advice.
Technical Report TR71704, Princeton University Computer Science,
December 2004.
[ Project
PDF ]
We take one of the first steps towards developing a
practical, staticallytyped, functional, aspectoriented
programming language by showing how to integrate polymorphism and
type analysis with aspectoriented programming features. In
particular, we demonstrate how to define typesafe polymorphic
advice using pointcuts that unify a collection of polymorphic join
points. We also introduce a new mechanism for specifying
contextsensitive advice that involves pattern matching against the
current stack of activation records, and meshes well with
functional programming idioms. We give our language meaning via a
typedirected translation into an expressive, but fairly simple,
typesafe intermediate language. Many complexities of the source
language are eliminated in this translation, leading to a modular
specification of its semantics. One of the novelties of the
intermediate language is the definition of polymorphic labels for
marking controlflow points. These labels are organized in a tree
structure such that a parent in the tree serves as a representative
for the collection of all its children. Type safety requires that
the type of each child is a generic instance of the type of the
polymorphic parent. Similarly, when a set of labels is assembled
as a pointcut, the type of each label is an instance of the type of
the pointcut.

[16]

Liang Huang and Stephanie Weirich.
A Design for TypeDirected Programming in Java (Extended
Version).
Technical Report MSCIS0411, University of Pennsylvania, Computer
and Information Science, October 2004.
[ PDF
PS ]

[17]

Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich.
An Open and Shut Typecase (Extended Version).
Technical Report MSCIS0426, University of Pennsylvania, Computer
and Information Science, October 2004.
[ PDF ]
Adhoc polymorphism is a compelling addition to typed programming languages. There are two different forms of adhoc polymorphism. With the nominal form, the execution of an operation is determined solely by the name of the type argument, whereas with the structural form, operations are defined by case analysis on the structure of types. The two forms differ in the way that they treat userdefined types. Operations defined by the nominal approach are considered "open"the programmer can add cases for new types without modifying existing code. The operations must be extended however with specialized code for the new types, and it may be tedious and even difficult to add extensions that apply to a potentially large universe of userdefined types. Structurally defined operations apply to new types by treating them as equal to their underlying definitions, so no new cases for new types are necessary. However this form is considered "closed" to extension, as the behaviour of the operations cannot be differentiated for the new types. This form destroys the distinctions that userdefined types are designed to express. Both approaches have their benefits, so it is important to provide both capabilities in a single language that is expressive enough to decouple the "openness" issue from the way that userdefined types are treated. We present such a language that supports both forms of adhoc polymorphism.

[18]

Simon L. Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.
Wobbly types: Practical Type Inference for Generalised Algebraic
Dataypes.
Technical Report MSCIS0526, University of Pennsylvania, Computer
and Information Science Department, Levine Hall, 3330 Walnut Street,
Philadelphia, Pennsylvania, 191046389, July 2004.
[ PDF ]
Generalised algebraic data types (GADTs), sometimes known as “guarded
recursive data types” or “firstclass phantom types”, are a simple
but powerful generalisation of the data types of Haskell and ML.
Recent works have given compelling examples of the utility of GADTs,
although type inference is known to be difficult.
It is time to pluck the fruit. Can GADTs be added to Haskell, without
losing type inference, or requiring unacceptably heavy type annotations?
Can this be done without completely rewriting the alreadycomplex Haskell
typeinference engine, and without complex interactions with (say)
type classes? We answer these questions in the affirmative, giving
a type system that explains just what type annotations are required,
and a prototype implementation that implements it. Our main technical
innovation is wobbly types, which express in a declarative way
the uncertainty caused by the incremental nature of typical typeinference
algorithms.

[19]

Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higherorder Abstract Syntax with
Parametric Polymorphism (Extended version).
Technical Report MSCIS0326, University of Pennsylvania, Computer
and Information Science, September 2003.
[ PDF
PS ]
Higherorder abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as captureavoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higherorder abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.
In this paper, we show how firstclass polymorphism can be used to guarantee the parametricity of functions embedded in higherorder abstract syntax. With this restriction, we implement a library of iteration operators over datastructures containing functionals. From this implementation, we derive "fusion laws" that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schuermann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System Fomega. This encoding can serve as a starting point for reasoning about higherorder structures in polymorphic languages.

[20]

Michael Hicks and Stephanie Weirich.
A Calculus for Dynamic Loading.
Technical Report MSCIS0007, University of Pennsylvania, April
2000.
[ PDF ]
We present the loadcalculus, used to model dynamic loading, and prove it sound. The calculus extends the polymorphic lambdacalculus with a load primitive that dynamically loads terms that are closed, with respect to values. The calculus is meant to approximate the process of dynamic loading in TAL/Load , a version of Typed Assembly Language extending with dynamic linking. To model the key aspects of TAL, the calculus contains references and facilities for named types. Loadable programs may refer to named types defined by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al. This calculus has been implemented in the TALx86 version of Typed Assembly Language, and is used to implement a fullfeatured dynamic linking library, DLpop.

[21]

Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics (Extended
Version).
Technical Report TR981721, Cornell University, Computer Science,
November 1998.
[ PDF
PS ]

