Stephanie Weirich's Publications
Copyright Information
Works in Progress
[1] Yiyun Liu, Jonathan Chan, and Stephanie Weirich. Indistinguishability in Predicative Type Theory. Draft, July 2024.
[2] Yiyun Liu and Stephanie Weirich. Functional Pearl: A Short and Mechanized Logical Relation for Dependent Type Theories. Draft, February 2024. [ PDF  http ]

Refereed Journal, Conference and Workshop Publications
[1] Jonathan Chan and Stephanie Weirich. Stratified Type Theory. In Viktor Vafeiadis, editor, European Symposium on Programming Languages and Systems, ESOP 2025, May 2025. To Appear.
[2] Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich. Effects and Coeffects in Call-By-Push-Value. Proc. ACM Program. Lang., 8(OOPSLA), October 2024. To Appear.
[3] Li-Yao Xia, Laura Israel, Maite Kramarz, Nathan Coltharp, Koen Claessen, Stephanie Weirich, and Yao Li. Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. Proc. ACM Program. Lang., 8(ICFP), August 2024. [ DOI  PDF ]
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki’s banker’s queue, and the implicit queue. We formally prove that the banker’s queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist’s method, a novel variant of the classical physicist’s method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.

Keywords: formal verification, computation cost, lazy evaluation, amortized analysis

[4] Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich. Internalizing Indistinguishability with Dependent Types. Proc. ACM Program. Lang., 8(POPL), January 2024. [ DOI  PDF ]
In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is indistinguishability: a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.

Keywords: Coq, Dependent Types, Formalization, Modes

[5] Yiyun Liu and Stephanie Weirich. Dependently-Typed Programming with Logical Equality Reflection. Proc. ACM Program. Lang., 7(ICFP), August 2023. [ DOI  PDF ]
In dependently-typed functional programming languages that allow general recursion, programs used as proofs must be evaluated to retain type soundness. As a result, programmers must make a trade-off between performance and safety. To address this problem, we propose System DE, an explicitly-typed, moded core calculus that supports termination tracking and equality reflection. Programmers can write inductive proofs about potentially diverging programs in a logical sublanguage and reflect those proofs to the type checker, while knowing that such proofs will be erased by the compiler before execution. A key feature of System DE is its use of modes for both termination and relevance tracking, which not only simplifies the design but also leaves it open for future extension. System DE is suitable for use in the Glasgow Haskell Compiler, but could serve as the basis for any general purpose dependently-typed language.

Keywords: Modes, Equality Reflection, Haskell, Dependent Types

[6] Yao Li and Stephanie Weirich. Program Adverbs and Tlön Embeddings. Proc. ACM Program. Lang., 6(ICFP), September 2022. Distinguished Paper Award. Artifact available. [ DOI  PDF ]
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves? In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tlön embeddings. Compared with embeddings based on free monads, Tlön embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program’s syntactic structure.

[7] Pritam Choudhury, Harley Eades III, and Stephanie Weirich. A Dependent Dependency Calculus. In Ilya Sergey, editor, Programming Languages and Systems, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 403--430, Cham, 2022. Springer International Publishing. Artifact available. [ DOI  http ]
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.

[8] Yao Li, Li-yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths. Proc. ACM Program. Lang., 5(ICFP), August 2021. [ DOI  PDF ]
Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program’s computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.

[9] Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee. An Existential Crisis Resolved: Type inference for first-class existential types. Proc. ACM Program. Lang., 5(ICFP), August 2021. Distinguished Paper Award. [ DOI  PDF ]
Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.

[10] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, and Stephanie Weirich. Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell Code. Journal of Functional Programming, 31:1--40, February 2021. [ DOI  .pdf ]
[11] Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie Weirich. A Graded Dependent Type System with a Usage-Aware Semantics. Proc. ACM Program. Lang., 5(POPL), January 2021. Artifact available. [ DOI  http ]
[12] Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-equivalence in Core Dependent Haskell. In Marc Bezem and Assia Mahboubi, editors, Post-proceedings of the 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics, pages 7:1--7:32, Dagstuhl, Germany, sep 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [ DOI  http ]
[13] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg. A Role for Dependent Types in Haskell. Proc. ACM Program. Lang., 3(ICFP), 2019. [ DOI  .pdf ]
[14] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell Code (Experience Report). Proc. ACM Program. Lang., 2(ICFP):89:1--89:16, July 2018. Artifact Available. [ DOI  http ]
Keywords: Coq, Haskell, verification

[15] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total Haskell is Reasonable Coq. In Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'18). ACM, 2018. New York, NY, USA. [ DOI  PDF ]
[16] Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A Specification for Dependent Types in Haskell. Proc. ACM Program. Lang., 1(ICFP):31:1--31:29, August 2017. Artifact evaluated as "Available" and Reusable". [ DOI  http ]
Keywords: Dependent Types, Haskell

[17] Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. [ DOI  arXiv  http ]
We introduce our efforts within the project The science of deep specification to work out the key formal underpinnings of industrial-scale formal specifications of software and hardware components, anticipating a world where large verified systems are routinely built out of smaller verified components that are also used by many other projects. We identify an important class of specification that has already been used in a few experiments that connect strong component-correctness theorems across the work of different teams. To help popularize the unique advantages of that style, we dub it deep specification, and we say that it encompasses specifications that are rich, two-sided, formal and live (terms that we define in the article). Our core team is developing a proof-of-concept system (based on the Coq proof assistant) whose specification and verification work is divided across largely decoupled subteams at our four institutions, encompassing hardware microarchitecture, compilers, operating systems and applications, along with cross-cutting principles and tools for effective specification. We also aim to catalyse interest in the approach, not just by basic researchers but also by users in industry.This article is part of the themed issue Verified trustworthy software systems.

[18] Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible Type Application. In European Symposium on Programming (ESOP), pages 229--254, April 2016. [ DOI  PDF ]
[19] Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers. Needle and Knot: Binder Boilerplate Tied Up. In European Symposium on Programming (ESOP), pages 419--445, April 2016. [ DOI ]
[20] Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis. A Reflection on Types. In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, editors, WadlerFest 2016: A list of successes that can change the world, LNCS, pages 292--317. Springer, 2016. [ DOI  PDF ]
[21] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe zero-cost coercions for Haskell. Journal of Functional Programming, 26, 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 run-time representation with some base type. We present a new mechanism that allows for zero-cost 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.

[22] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence. In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 369--382, Mumbai, India, January 2015. Artifact Evaluated. [ DOI  PDF ]
[23] Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee. Verified ROS-Based Deployment of Platform-Independent Control Systems. In Seventh NASA Formal Methods Symposium, pages 248--262, Pasadena, CA, 2015. [ PDF ]
[24] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining Proofs and Programs in a Dependently Typed Language. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, page 33–45, New York, NY, USA, 2014. Association for Computing Machinery. [ DOI  .pdf ]
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and "mobile" program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.

Keywords: termination, dependent types, general recursion

[25] Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. Closed type families with overlapping equations. In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 671--683, San Diego, CA, USA, January 2014. [ PDF ]
[26] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe Zero-Cost Coercions for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, page 189–202, New York, NY, USA, 2014. Association for Computing Machinery. [ DOI  http ]
Generative 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 run-time representation with some base type. We present a new mechanism that allows for zero-cost 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.

Keywords: type class, coercion, newtype deriving, haskell

[27] 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 call-by-value semantics. Progress in Informatics, (10):19--48, March 2013. [ http ]
[28] Zhengjiang Hu, Shin-Cheng Mu, and Stephanie Weirich. Guest Editorial: Advanced programming techniques for construction of robust, generic and evolutionary programs. Progress in Informatics, (10):1--2, March 2013. [ DOI  http ]
[29] 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 platform-aware attack-resilient control systems: extended abstract. In HiCoNS '13: Proceedings of the 2nd ACM international conference on High confidence networked systems, pages 75--76, New York, NY, USA, 2013.
[30] 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, page 275–286, New York, NY, USA, 2013. Association for Computing Machinery. [ DOI  PDF  http ]
System FC, the core language of the Glasgow Haskell Compiler, is an explicitly-typed variant of System F with first-class type equality proofs called coercions. This extensible proof system forms the foundation for type system extensions such as type families (type-level functions) and Generalized Algebraic Datatypes (GADTs). Such features, in conjunction with kind polymorphism and datatype promotion, support expressive compile-time reasoning.However, the core language lacks explicit kind equality proofs. As a result, type-level computation does not have access to kind-level functions or promoted GADTs, the type-level analogues to expression-level features that have been so useful. In this paper, we eliminate such discrepancies by introducing kind equalities to System FC. Our approach is based on dependent type systems with heterogeneous equality and the "Type-in-Type" axiom, yet it preserves the metatheoretic properties of FC. In particular, type checking is simple, decidable and syntax directed. We prove the preservation and progress theorems for the extended language.

Keywords: equality, dependent types, haskell

[31] Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell Symposium, pages 117--130, Copenhagen, Denmark, September 2012. [ PDF ]
[32] Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. Journal of Functional Programming, 22(3):225--274, May 2012.
[33] Stephanie Weirich and Chris Casinghino. Generic Programming with Dependent Types. In Jeremy Gibbons, editor, Generic and Indexed Programming, number 7470 in Lecture Notes in Computer Science, pages 217--258. Springer-Verlag Berlin Heidelberg, 2012. [ PDF ]
[34] 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 53--66, 2012. [ PDF ]
[35] 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 Call-by-value Semantics. In Sixth ACM SIGPLAN Workshop Programming Languages meets Program Verification (PLPV '12), pages 15--26, 2012. [ PDF ]
[36] 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 Call-by-value Dependent Type Systems. In Fourth workshop on Mathematically Structured Functional Programming (MSFP '12), pages 112--162, 2012. [ PDF ]
[37] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Step-Indexed Normalization for a Language with General Recursion. In Fourth workshop on Mathematically Structured Functional Programming (MSFP '12), pages 25--39, 2012. [ PDF ]
[38] Umut A. Acar, James Cheney, and Stephanie Weirich. Editorial - Special issue dedicated to ICFP 2010. J. Funct. Program., 22(4-5):379--381, 2012. [ DOI ]
[39] Benjamin C. Pierce and Stephanie Weirich. Preface to Special Issue on the POPLMark Challenge. J. Autom. Reasoning, 49(3):301--302, 2012.
[40] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level Computation. In POPL 11: 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, January 26--28, 2011. Austin, TX, USA., pages 227--240, 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 well-established feature is in tension with the non-parametric 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 non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

[41] 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 333--345, New York, NY, USA, 2011. [ PDF ]
Keywords: generic programming, haskell, name binding, patterns

[42] Tim Sheard, Aaron Stump, and Stephanie Weirich. Language-Based Verification Will Change The World. In 2010 FSE/SDP Workshop on the Future of Software Engineering Research, pages 343--348, November 2010. Position paper. [ PDF ]
[43] 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 76--93, Edinburgh, Scotland, July 2010. [ PDF ]
This paper proposes a type-and-effect 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 type-form “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 meta-theory 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.

[44] Dimitrios Vytiniotis and Stephanie Weirich. Parametricity, Type Equality and Higher-order Polymorphism. Journal of Functional Programming, 20(2):175--210, March 2010. [ PDF ]
Propositions that express type equality are a frequent ingredient of modern functional programming---they can encode generic functions, dynamic types, and GADTs. Via the Curry-Howard 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 higher-order 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.

[45] Stephanie Weirich and Chris Casinghino. Arity-generic type-generic programming. In ACM SIGPLAN Workshop on Programming Languages Meets Program Verification (PLPV), pages 15--26, January 2010. [ PDF ]
[46] Limin Jia, Jianzhou Zhao, Vilhem Sjöberg, and Stephanie Weirich. Dependent types and Program Equivalence. In 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 275--286, Madrid, Spain, January 2010. [ PDF ]
The definition of type equivalence is one of the most important design issues for any typed language. In dependently-typed 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 dependently-typed 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 beta-equivalence, to contextual equiva lence, to some exotic equivalences.

[47] Michael Greenberg, Benjamin Pierce, and Stephanie Weirich. Contracts Made Manifest. In 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 353--364, Madrid, Spain, January 2010. [ PDF ]
Since Findler and Felleisen introduced higher-order 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 equivalent---different 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 soundness---a substantial result in itself, for lambdah---and 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.

[48] 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 79--90, November 2009. [ PDF ]
Many programs operate reactively---patiently 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 client-side web applications, we explore definitions of noninterference for reactive programs and identify two of special interest---one corresponding to termination-insensitive noninterference for a simple sequential language, the other to termination-sensitive 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 information-flow type system and apply our proof technique to show that well-typed programs are secure.

[49] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH: First-class polymorphism for Haskell. In ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming, pages 295--306, Victoria, BC, Canada, September 2008. [ PDF ]
Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting “first-class” 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 higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; 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.

[50] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. AspectML: A Polymorphic Aspect-oriented Functional Programming Language. ACM Transactions on Programming Languages, 30(3):1--60, May 2008. [ Project  PDF ]
This paper defines Aspectml, a typed functional, aspect-oriented programming language. The main contribution of Aspectml is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, Aspectml allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. Aspectml also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe 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 control-flow 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.

[51] Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3--15, January 2008. [ Project  PDF ]
Machine-checked 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 proof-carrying 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.

[52] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism. Journal of Functional Programming, 18(1):87--140, January 2008. [ PDF ]
Higher-order 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 capture-avoiding 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 first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures 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 F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

[53] Dimitrios Vytiniotis and Stephanie Weirich. Free theorems and runtime type representations. In Mathematical Foundations of Programming Semantics (MFPS XXIII), pages 357--373, 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 term-level 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 representation-based 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.

[54] 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 XVII--1---XVII--15. Dept. of Math and Computer Science, Seton Hall University, April 2007. TR-SHU-CS-2007-04-1. [ PDF ]
[55] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(1):1--82, 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 Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types --- that is, functions that take polymorphic functions as their arguments.

Complete type inference is known to be undecidable for higher-rank (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 lambda-calculus proposed by Odersky and Laufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on lambda-bound arguments and arbitrary sub-terms. 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 higher-rank types become eminently usable.

Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference 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.

[56] Stephanie Weirich. Type-Safe Run-time Polytypic Programming. Journal of Functional Programming, 16(10):681--710, November 2006. [ PDF ]
Polytypic programming is a way of defining type-indexed operations, such as map, fold and zip, based on type information. Run-time polytypic programming allows that type information to be dynamically computed---this support is essential in modern programming languages that support separate compilation, first-class type abstraction, or polymorphic recursion.

However, in previous work we defined run-time polytypic programming with a type-passing semantics. Although it is natural to define polytypic programs as operating over first-class types, such a semantics suffers from a number of drawbacks. This paper describes how to recast that work in a type-erasure semantics, where terms represent type information in a safe manner. The resulting language is simple and easy to implement---we present a prototype implementation of the necessary machinery as a small Haskell library.

[57] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP), pages 50--61, Portland, OR, USA, September 2006. [ PDF ]
Generalized algebraic data types (GADTs), sometimes known as “guarded recursive data types” or “first-class 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 programmer-supplied 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 type-inference algorithms.

[58] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Boxy type inference for higher-rank types and impredicativity. In International Conference on Functional Programming (ICFP), pages 251--262, 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 programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidirectional propagation of type annotations. The result is a type system that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.

[59] Geoffrey Washburn and Stephanie Weirich. Good Advice for Type-directed Programming: Aspect-oriented Programming and Extensible Generic Functions. In Workshop on Generic Programming (WGP), pages 33--44, Portland, OR, USA, September 2006. [ Project  PDF ]
Type-directed programming is an important idiom for software design. In type-directed 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.

Type-directed 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 type-directed functions that are closed to extension. However, Lämmel and Peyton Jones recently developed a technique for writing openly extensible type-directed 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 type-directed functions by using the aspect-oriented 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 type-directed functions to be extended at any time with cases for types that were not even known at compile-time. This capability is critical to writing programs that make use of dynamic loading or runtime type generativity.

[60] Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1--12, 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 built-in 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 pattern-matches a representation types. Furthermore, operations defined in this manner are extensible---instances 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.

[61] Brian Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal Reasoning Techniques in Coq. In International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP), pages 60--69, Seattle, WA, USA, August 2006. [ Project  PDF ]
We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in 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.

[62] 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 26--30, 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.

[63] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. PolyAML: A polymorphic aspect-oriented functional programmming language. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 306--319, Tallinn, Estonia, September 2005. [ Project  PDF  PS ]
This paper defines PolyAML, a typed functional and aspect-oriented programming language. The main contribution of PolyAML is in the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. In order to support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe 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 control-flow 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.

[64] 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 50--65, 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 machine-checked proofs?

We propose a concrete set of benchmarks for measuring progress in this area. Based on the metatheory of System F-sub, a typed lambda-calculus with second-order 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.

[65] Geoffrey Washburn and Stephanie Weirich. Generalizing Parametricity Using Information Flow. In Twentieth Annual IEEE Symposium on. Logic in Computer Science (LICS 2005), pages 62--71, Chicago, IL, USA, June 2005. [ Project  PDF  PS ]
Run-time 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 run-time 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.

[66] Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An Open and Shut Typecase. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 13--24, Long Beach, CA, USA, January 2005. [ PS ]
Two different ways of defining ad-hoc 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 user-defined 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 ad-hoc polymorphism, using the same basic constructs.

[67] Stephanie Weirich. Type-Safe Cast. Journal of Functional Programming, 14(6):681--695, 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 run-time 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 higher-order polymorphism, a casting function can treat its argument parametrically. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and Haskell type classes.

[68] Stephanie Weirich and Liang Huang. A Design for Type-Directed Java. In Viviana Bono, editor, Workshop on Object-Oriented Developments (WOOD), ENTCS, pages 117--136, August 2004. [ Project  PDF  PS ]
Type-directed 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 updated---they 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 run-time classes of objects. However, the Java mechanisms for type-directed 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 type-directed programming in Java, and show that these mechanisms are sound when included in a language similar to Featherweight Java. Basically, these new mechanisms pattern-match the name and structure of the type parameters of generic code, instead of the run-time 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 run-time type of an object, our mechanisms allow any supertype to be supplied for analysis, hiding its precise structure.

[69] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 249--262, Uppsala, Sweden, August 2003. [ PDF  PS ]
Higher-order 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 capture-avoiding 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 higher-order 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 first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures 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 F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

[70] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type Erasure Semantics. Journal of Functional Programming, 12(6):567--600, 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 tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing 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 type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time 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 beta-expansions required by other frameworks.

[71] Stephanie Weirich. Higher-Order Intensional Type Analysis. In Daniel Le Métayer, editor, 11th European Symposium on Programming (ESOP), pages 98--114, 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 higher-order and kind-polymorphic 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.

[72] Stephanie Weirich. Encoding Intensional Type Analysis. In D. Sands, editor, 10th European Symposium on Programming (ESOP), pages 92--106, Genova, Italy, April 2001. [ PDF  PS  http ]
Languages for intensional type analysis permit ad-hoc polymorphism, or run-time analysis of types. However, such languages require complex, specialized constructs to support this operation, which hinder optimization and complicate the meta-theory 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.

[73] Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and Flexible Dynamic Linking of Native Code. In R. Harper, editor, Types in Compilation: Third International Workshop, TIC 2000; Montreal, Canada, September 21, 2000; Revised Selected Papers, volume 2071 of Lecture Notes in Computer Science, pages 147--176. Springer, 2001. [ PDF  PS  http ]
We present the design and implementation of the first complete framework for flexible and safe dynamic linking of native code. Our approach extends Typed Assembly Language with a primitive for loading and typechecking code, which is flexible enough to support a variety of linking strategies, but simple enough that it does not significantly expand the trusted computing base. Using this primitive, along with the ability to compute with types, we show that we can program many existing dynamic linking approaches. As a concrete demonstration, we have used our framework to implement dynamic linking for a type-safe dialect of C, closely modeled after the standard linking facility for Unix C programs. Aside from the unavoidable cost of verification, our implementation performs comparably with the standard, untyped approach.

[74] Stephanie Weirich. Type-Safe Cast: Functional Pearl. In Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 58--67, Montreal, Canada, September 2000. [ PDF  PS ]
In a language with non-parametric or ad-hoc 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 higher-order type abstraction. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and type classes.

[75] Karl Crary and Stephanie Weirich. Resource Bound Certification. In The Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 184--198, 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 control-flow 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 source-level programs. The principal device in our approach is a strategy for simulating dependent types using sum and inductive kinds.

[76] Karl Crary and Stephanie Weirich. Flexible Type Analysis. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 233--248, Paris, France, September 1999. [ PDF  PS ]
Run-time type dispatch enables a variety of advanced optimization techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, and flattened data structures. However, modern type-preserving 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 previous-stage 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 type-erasure semantics.

[77] 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 25--35, 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 low-level, 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 (32-bit 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 high-level language features are compiled to TALx86. For this purpose, we present a type-safe C-like language called Popcorn.

[78] 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 301--313, 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 tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing 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 type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time 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 beta-expansions required by other frameworks.

[79] 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 23--32, 1996. [ PDF  PS ]
MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations tha may cause run-time errors suce as dereferencing the null pointer or applying non-functions. 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.


Book Chapters
[1] Stephanie Weirich. Type Systems. In Teofilo F. Gonzalez, Jorge Diaz-Herrera, and Allen Tucker, editors, Computing Handbook, 3rd ed. (1), pages 70:1--39. CRC Press, 2014.

Misc
[1] Stephanie Weirich. Tracking how dependently-typed functions use their arguments, 2024. Invited keynote at LICS/ICALP/FSCD.
[2] Emmanuel Suárez Acevedo and Stephanie Weirich. Making Logical Relations More Relatable (Proof Pearl), September 2023. [ arXiv ]
[3] Stephanie Weirich. Implementing Dependent Types in pi-forall, 2023. Lecture notes for the Oregon Programming Languages Summer School. [ DOI  http ]
[4] Stephanie Weirich and Benjamin Pierce. ICFP 2020 Post-Conference Report, 2021. [ arXiv  http ]
[5] Antal Spector-Zabusky, Joachim Breitner, Yao Li, and Stephanie Weirich. Embracing a mechanized formalization gap, October 2019. [ arXiv ]
[6] Anastasiya Kravchuk-Kirilyuk Stephanie Weirich, Antoine Voizard. Locally Nameless at Scale. The Fourth International Workshop on Coq for Programming Languages, January 2018. [ PDF ]
[7] Stephanie Weirich. The Influence of Dependent Types, January 2017. Invited keynote given at POPL 2017.
[8] Stephanie Weirich. Depending on Types, 2014. Invited keynote given at ICFP 2014.
[9] Stephanie Weirich. Designing Dependently-Typed Programming Languages. Lectures given at the Summer School on Logic and Theorem Proving in Programming Languages, Eugene OR, USA. July 2013, July 2013.
[10] Stephanie Weirich. Dependently typed programming in GHC, May 2012. Invited keynote given at FLOPS 2012.
[11] Kathleen Fisher, Ronald Garcia, and Stephanie Weirich. Nourishing the future of the field: the programming language mentoring workshop 2012, April 2012. [ DOI ]
[12] Stephanie Weirich. Combining Proofs and Programs, June 2011. Joint invited speaker for Rewriting Techniques and Applications (RTA 2011) and Typed Lambda Calculi and Applications (TLCA 2011).
[13] Stephanie Weirich. ICFP 2010 PC Chair's Report, September 2010.
[14] Brian Aydemir and Stephanie Weirich. LNgen: Tool Support for Locally Nameless Representations, June 2010. [ Project  PDF ]
[15] Stephanie Weirich. Haskell 2009 PC Chair's Report, August 2009.
[16] Brian Aydemir, Steve Zdancewic, and Stephanie Weirich. Abstracting Syntax, March 2009. [ Project  PDF ]
[17] Brian Aydemir, Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic. Using Proof Assistants for Programming Language Research or, How to write your Next POPL paper in Coq. Tutorial session co-located with POPL 2008, San Francisco, CA, January 2008. Tutorial materials available at http://www.cis.upenn.edu/~plclub/popl08-tutorial/.
[18] Stephanie Weirich and Brian Aydemir. Coq for Programming Language Metatheory. Lectures given at the Summer School on Logic and Theorem Proving in Programming Languages, Eugene OR, USA. July 22-25, 2008, 2008. Tutorial materials available at http://www.cis.upenn.edu/~plclub/oregon08/.
[19] Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. Manifest Security, January 2007. White paper. [ PDF ]

Thesis
[1] Stephanie Weirich. Programming With Types. PhD thesis, Cornell University, August 2002. [ PDF  PS ]
Run-time type analysis is an increasingly important linguistic mechanism in modern programming languages. Language runtime systems use it to implement services such as accurate garbage collection, serialization, cloning and structural equality. Component frameworks rely on it to provide reflection mechanisms so they may discover and interact with program interfaces dynamically. Run-time type analysis is also crucial for large, distributed systems that must be dynamically extended, because it allows those systems to check program invariants when new code and new forms of data are added. Finally, many generic user-level algorithms for iteration, pattern matching, and unification can be defined through type analysis mechanisms.

However, existing frameworks for run-time type analysis were designed for simple type systems. They do not scale well to the sophisticated type systems of modern and next-generation programming languages that include complex constructs such as first-class abstract types, recursive types, objects, and type parameterization. In addition, facilities to support type analysis often require complicated language semantics that allow little freedom in their implementation. This dissertation investigates the foundations of run-time type analysis in the context of statically-typed, polymorphic programming languages. Its goal is to show how such a language may support type-analyzing operations in a way that balances expressiveness, safety and simplicity.


Artifacts, Extended Versions, and Technical Reports
[1] Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich. Artifact associated with "Effects and Coeffects in Call-By-Push-Value". Technical report, July 2024. [ DOI  http ]
[2] Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, and Yao Li. Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs (Artifact). Technical report, June 2024. [ DOI  http ]
[3] Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich. Artifact associated with Internalizing Indistinguishability with Dependent Types. Technical report, October 2023. Awarded “Available” and “Evaluated & Reusable” badges by POPL 2024 Artifact Evaluation Committee. [ DOI  http ]
[4] Yiyun Liu and Stephanie Weirich. Artifact Associated with Dependently-Typed Programming with Logical Equality Reflection. Technical report, 2023. Awarded “Available” and “Evaluated & Reusable” badges by ICFP 2023 Artifact Evaluation Committee. [ DOI  http ]
This artifact contains the complete mechanized Coq proofs of the lemmas and theorems about System DE. The VM image is preinstalled with the dependencies required to build and verify the Coq development.

Keywords: Coq, Dependent types, Mechanized metatheory

[5] Yao Li and Stephanie Weirich. Program Adverbs and Tlön Embeddings (artifact). Technical report, June 2022. Awarded “Available” and “Evaluated & Reusable” badges by ICFP 2023 Artifact Evaluation Committee. [ DOI ]
[6] Pritam Choudhury, Harley Eades III, and Stephanie Weirich. Artifact Associated with A Dependent Dependency Calculus. Technical report, January 2022. Awarded “Reusable” and “Available” badges by ESOP 2022 Artifact Evaluation Committee. [ DOI ]
[7] Yao Li, Li yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths (artifact). Technical report, May 2021. Awarded “Functional” and “Available” badges by ICFP 2021 Artifact Evaluation Committee. [ DOI ]
[8] Yao Li, Li-yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths. Technical report, March 2021. [ arXiv  http ]
[9] Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. Artifact for “A Graded Dependent Type System with a Usage-Aware Semantics”. Technical report, December 2020. Awarded “Reusable”, “Functional” and “Available” badges by POPL 2021 Artifact Evaluation Committee. [ DOI ]
[10] Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie Weirich. A Graded Dependent Type System with a Usage-Aware Semantics (Extended Version). Technical report, 2020. [ http ]
[11] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. Replication Package for Article: A Role for Dependent Types in Haskell. Technical report, July 2019. Awarded “Functional” and “Available” badges by ICFP 2019 Artifact Evaluation Committee. [ DOI ]
[12] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg. A Role for Dependent Types in Haskell (Extended Version). Technical report, 2019. [ http ]
[13] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, and Stephanie Weirich. The hs-to-coq tool with examples. Technical report, July 2018. Awarded “Artifacts Available” and “Artifacts Evaluated - Functional” badges by ICFP 2018 Artifact Evaluation Committee. [ DOI ]
[14] Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible Type Application (Extended version). Technical report, January 2016. [ PDF ]
[15] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence (Extended Version). Technical Report MS-CIS-14-10, University of Pennsylvania, October 2014. [ PDF ]
[16] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe Zero-cost Coercions for Haskell (Extended Version). Technical Report MS-CIS-14-07, Univ. of Pennsylvania, April 2014. [ PDF ]
[17] Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. Closed type families with overlapping equations (Extended version). Technical Report MS-CIS-13-10, University of Pennsylvania, November 2013. [ PDF ]
[18] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining Proofs and Programs in a Dependently Typed Language (With Technical Appendix). Technical Report MS-CIS-13-08, University of Pennsylvania, November 2013. [ PDF ]
[19] Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System FC with explicit kind equality (Extended Version). Technical report, September 2013. [ PDF ]
[20] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level 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 well-established feature is in tension with the non-parametric 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 non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

[21] Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. Termination Casts: A Flexible Approach to Termination with General Recursion (Technical Appendix). Technical Report MS-CIS-10-21, University of Pennsylvania Department of Computer and Information Science, 2010. [ PDF ]
[22] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Simple unification-based type inference for GADTs, Technical Appendix. Technical Report MS-CIS-05-22, University of Pennsylvania, April 2006. [ PDF ]
[23] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Boxy type inference for higher-rank types and impredicativity, Technical Appendix. Technical Report MS-CIS-05-23, University of Pennsylvania, April 2006. [ PDF ]
[24] Geoffrey Washburn and Stephanie Weirich. Generalizing Parametricity Using Information Flow (Extended version). Technical Report MS-CIS-05-04, Computer and Information Science, University of Pennsylvania, July 2005. [ PDF ]
Run-time 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 run-time 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.

[25] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types (Technical appendix). Technical Report MIS-CIS-05-14, University of Pennsylvania, July 2005. [ Project  PDF ]
[26] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. PolyAML: A Polymorphic Aspect-Oriented Functional Programming Language (Extended Version). Technical Report MS-CIS-05-07, University of Pennsylvania, Department of Computer and Information Science, 2005. [ PDF ]
This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe 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 control-flow 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.

[27] Dan S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. Analyzing Polymorphic Advice. Technical Report TR-717-04, Princeton University Computer Science, December 2004. [ Project  PDF ]
We take one of the first steps towards developing a practical, statically-typed, functional, aspect-oriented programming language by showing how to integrate polymorphism and type analysis with aspect-oriented programming features. In particular, we demonstrate how to define type-safe polymorphic advice using pointcuts that unify a collection of polymorphic join points. We also introduce a new mechanism for specifying context-sensitive 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 type-directed translation into an expressive, but fairly simple, type-safe 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 control-flow 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.

[28] Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An Open and Shut Typecase (Extended Version). Technical Report MS-CIS-04-26, University of Pennsylvania, Computer and Information Science, October 2004. [ PDF ]
Ad-hoc polymorphism is a compelling addition to typed programming languages. There are two different forms of ad-hoc 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 user-defined 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 user-defined 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 user-defined 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 user-defined types are treated. We present such a language that supports both forms of ad-hoc polymorphism.

[29] Liang Huang and Stephanie Weirich. A Design for Type-Directed Programming in Java (Extended Version). Technical Report MS-CIS-04-11, University of Pennsylvania, Computer and Information Science, October 2004. [ PDF  PS ]
[30] Simon L. Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: Practical Type Inference for Generalised Algebraic Dataypes. Technical Report MS-CIS-05-26, University of Pennsylvania, Computer and Information Science Department, Levine Hall, 3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389, July 2004. [ PDF ]
Generalised algebraic data types (GADTs), sometimes known as “guarded recursive data types” or “first-class 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 already-complex Haskell type-inference 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 type-inference algorithms.

[31] Geoffrey Washburn and Stephanie Weirich. Unifying nominal and structural ad-hoc polymorphism (Extended version). Technical report, University of Pennsylvania, March 2004. [ PDF ]
Ad-hoc polymorphism allows the execution of programs to depend on type information. In modern systems, it is useful for implementing generic operations over data structures, such as equality, marshalling, or traversal. In the past, there have been two different forms of ad-hoc polymorphism. The nominal form dispatches on the name of the type argument, whereas the structural form operates by decomposing the structure of types. In languages with user-defined types, these two approaches are very different. Operations defined by the nominal approach are “open”---they must be extended with specialized branches for user-defined types. In contrast, structurally defined operations are closed to extension. They automatically apply to user-defined types by treating them as their underlying definitions. Both approaches have their benefits, so it important to provide both capabilities in a language. Therefore we present an expressive language that supports both forms of ad-hoc polymorphism in a single framework. Among the language's features are the ability to define both “open” and “closed” operations with a single mechanism, the ability to naturally restrict the domain of type-analyzing operations, and new mechanisms for defining higher-order polytypism and manipulating generative type definitions.

[32] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism (Extended version). Technical Report MS-CIS-03-26, University of Pennsylvania, Computer and Information Science, September 2003. [ PDF  PS ]
Higher-order 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 capture-avoiding 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 higher-order 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 first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures 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 F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

[33] Michael Hicks and Stephanie Weirich. A Calculus for Dynamic Loading. Technical Report MS-CIS-00-07, University of Pennsylvania, April 2000. [ PDF ]
We present the load-calculus, used to model dynamic loading, and prove it sound. The calculus extends the polymorphic lambda-calculus 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 full-featured dynamic linking library, DLpop.

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

Copyright Information
The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Parts of this page were generated by bibtex2html Last modified: Thu Aug 22 08:28:48 EDT 2024