Weirich, Stephanie
Loading...
Email Address
ORCID
Disciplines
Programming Languages and Compilers
relationships.isProjectOf
relationships.isOrgUnitOf
Position
Professor
Introduction
Research Interests
Functional Programming
Type Systems
Type Systems
Collection
36 results
Search Results
Now showing 1 - 10 of 36
Publication Irrelevance, Heterogeneous Equity, and Call-by-value Dependent Type Systems(2012-01-01) Sjoberg, Vilhelm; Casinghino, Chris; Collins, Nathan; Ahn, Ki Yung; Sheard, Tim; Eades, Harley D; Fu, Peng; Kimmell, Garrin; Stump, Aaron; Weirich, StephanieWe present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form.Publication Towards Synthesis of Platform-Aware Attack-Resilient Control Systems: Extended Abstract(2013-04-09) Pajic, Miroslav; Bezzo, Nicola; Weimer, James; Alur, Rajeev; Mangharam, Rahul; Michael, Nathan; Pappas, George J; Sokolsky, Oleg; Tabuada, Paulo; Weirich, Stephanie; Lee, InsupPublication Parametricity, Type Equality and Higher-order Polymorphism(2010-03-01) Vytiniotis, Dimitrios; Weirich, StephaniePropositions 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 re ect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to 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.Publication Giving Haskell a Promotion(2012-01-28) Weirich, Stephanie; Yorgey, Brent A; Cretin, Julien; Peyton Jones, Simon; Vytiniotis, Dimitrios; Magalhaes, Jose PStatic type systems strive to be richly expressive while still being simple enough for programmers to use. We describe an experiment that enriches Haskell’s kind system with two features promoted from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.Publication Generalizing Parametricity Using Information-flow(2005-06-26) Washburn, Geoffrey; Weirich, Stephanie CRun-time type analysis allows programmers to easily and concisely define 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: clients can determine the structure of these supposedly "abstract" data types. Furthermore, access control mechanisms do not help isolate the implementation of abstract datatypes from their clients. Buggy or malicious authorized modules may leak type information to unauthorized clients, so module implementors cannot reliably tell which parts of a program rely on their type definitions. Currently, module implementors rely on parametric polymorphism to provide integrity and confidentiality guarantees about their abstract datatypes. However, standard parametricity does not hold for languages with run-time type analysis; this paper shows how to generalize parametricity so that it does. The key is to augment the type system with annotations about information-flow. Implementors can then easily see which parts of a program depend on the chosen implementation by tracking the flow of dynamic type information.Publication Combining Proofs and Programs in a Dependently Typed Language(2013-01-01) Weirich, Stephanie; Sjoberg, Vilhelm; Casinghino, ChrisMost 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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory Keywords Dependent types; Termination; General recursionPublication Verified ROS-Based Deployment of Platform-Independent Control Systems(2015-04-27) Park, Junkil; Sokolsky, Oleg; Weirich, Stephanie; Meng, Wenrui; Lee, InsupThe paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always correctly connects the controller function to sensors and actuators in the robot. We use ROSGen to implement a cruise control system on the LandShark robot.Publication Binders Unbound(2011-09-19) Weirich, Stephanie; Yorgey, Brent A; Sheard, TimImplementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as -equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected. Furthermore, their implementations are tedious, requiring â boilerplateâ code that must be updated whenever the object language definition changes. Many researchers have therefore sought to specify binding syntax declaratively, so that tools can correctly handle the details behind the scenes. This idea has been the inspiration for many new systems (such as Beluga, Delphin, FreshML, FreshOCaml, C ml, FreshLib, and Ott) but there is still room for improvement in expressivity, simplicity and convenience. In this paper, we present a new domain-specific language, UNBOUND, for specifying binding structure. Our language is particularly expressiveâ it supports multiple atom types, pattern binders, type annotations, recursive binders, and nested binding (necessary for telescopes, a feature found in dependently-typed languages). However, our specification language is also simple, consisting of just five basic combinators. We provide a formal semantics for this language derived from a locally nameless representation and prove that it satisfies a number of desirable properties. We also present an implementation of our binding specification language as a GHC Haskell library implementing an embedded domain specific language (EDSL). By using Haskell type constructors to represent binding combinators, we implement the EDSL succinctly using datatype-generic programming. Our implementation supports a number of features necessary for practical programming, including flexibility in the treatment of user-defined types, besteffort name preservation (for error messages), and integration with Haskellâ s monad transformer library.Publication LNgen: Tool Support for Locally Nameless Representations(2010-06-01) Aydemir, Brian; Weirich, StephanieGiven the complexity of the metatheoretic reasoning about current programming languages and their type systems, techniques for mechanical formalization and checking of such metatheory have received much recent attention. In previous work, we advocated a combination of locally nameless representation and cofinite quantification as a lightweight style for carrying out such formalizations in the Coq proof assistant. As part of the presentation of that methodology, we described a number of operations associated with variable binding and listed a number of properties, called “infrastructure lemmas”, about those operations that needed to be shown. The proofs of these infrastructure lemmas are straightforward but tedious. In this work, we present LNgen, a prototype tool for automatically generating statements and proofs of infrastructure lemmas from Ott language specifications. Furthermore, the tool also generates a recursion scheme for defining functions over syntax, which was not available in our previous work. LNgen works in concert with Ott to effectively alleviate much of the tedium of working with locally nameless syntax. For the case of untyped lambda terms, we show that the combined output from the two tools is sound and complete, with LNgen automatically proving many of the key lemmas. We prove the soundness of our representation with respect to a fully concrete representation, and we argue that the representation is complete—that we generate the right set of lemmas—with respect to Gordon and Melham’s “Five Axioms of Alpha-Conversion.”Publication Termination Casts: A Flexible Approach to Termination With General Recursion (Technical Appendix)(2010-01-01) Stump, Aaron; Sjoberg, Vilhelm; Weirich, StephanieThis paper proposes a type-and-effect system called Teq↓, which 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 Teq↓ to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teq↓ is translated to a theorem expressing the appropriate termination property of the computational part of the Teq↓ term.