Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 12 of 12
Full-Text Articles in Physical Sciences and Mathematics
Dependent Types And Program Equivalence, Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg, Stephanie Weirich
Dependent Types And Program Equivalence, Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg, Stephanie Weirich
Stephanie Weirich
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, …
Generative Type Abstraction And Type-Level Computation, Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, Stephan A. Zdancewic
Generative Type Abstraction And Type-Level Computation, Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, Stephan A. Zdancewic
Stephanie Weirich
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.
Reactive Noninterference, Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjoberg, Stephanie Weirich, Stephan A. Zdancewic
Reactive Noninterference, Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjoberg, Stephanie Weirich, Stephan A. Zdancewic
Stephanie Weirich
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 …
Irrelevance, Heterogeneous Equity, And Call-By-Value Dependent Type Systems, Vilhelm Sjoberg, Chris Casinghino, Nathan Collins, Ki Yung Ahn, Tim Sheard, Harley D. Eades Iii, Peng Fu, Garrin Kimmell, Aaron Stump, Stephanie Weirich
Irrelevance, Heterogeneous Equity, And Call-By-Value Dependent Type Systems, Vilhelm Sjoberg, Chris Casinghino, Nathan Collins, Ki Yung Ahn, Tim Sheard, Harley D. Eades Iii, Peng Fu, Garrin Kimmell, Aaron Stump, Stephanie Weirich
Stephanie Weirich
We 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.
Contracts Made Manifest, Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich
Contracts Made Manifest, Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich
Stephanie Weirich
Since Findler and Felleisen (Findler, R. B. & Felleisen, M. 2002) introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen (2002) 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 …
Giving Haskell A Promotion, Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, Jose P. Magalhaes
Giving Haskell A Promotion, Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, Jose P. Magalhaes
Stephanie Weirich
Static 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.
Language-Based Verification Will Change The World, Tim Sheard, Aaron Stump, Stephanie Weirich
Language-Based Verification Will Change The World, Tim Sheard, Aaron Stump, Stephanie Weirich
Stephanie Weirich
We argue that lightweight, language-based verification is poised to enter mainstream industrial use, where it will have a major impact on software quality and reliability. We explain how language-based approaches based on so-called dependent types are already being adopted in functional programming languages, and why such methods will be successful for mainstream use, where traditional formal methods have failed.
Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino
Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino
Stephanie Weirich
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 …
Parametricity, Type Equality And Higher-Order Polymorphism, Dimitrios Vytiniotis, Stephanie Weirich
Parametricity, Type Equality And Higher-Order Polymorphism, Dimitrios Vytiniotis, Stephanie Weirich
Stephanie Weirich
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 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 …
Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich
Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich
Stephanie Weirich
This paper presents the design of ZOMBIE, a dependently-typed programming language that uses an adaptation of a congruence closure algorithm for proof and type inference. This algorithm allows the type checker to automatically use equality assumptions from the context when reasoning about equality. Most dependently typed languages automatically use equalities that follow from -reduction during type checking; however, such reasoning is incompatible with congruence closure. In contrast, ZOMBIE does not use automatic -reduction because types may contain potentially diverging terms. Therefore ZOMBIE provides a unique opportunity to explore an alternative definition of equivalence in dependently typed language design. Our work …
Equational Reasoning About Programs With General Recursion And Call-By-Value Semantics, Garrin Kimmell, Aaron Stump, Harley D. Eades Iii, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn
Equational Reasoning About Programs With General Recursion And Call-By-Value Semantics, Garrin Kimmell, Aaron Stump, Harley D. Eades Iii, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn
Stephanie Weirich
Dependently typed programming languages provide a mechanism for integrating verification and programming by encoding invariants as types. Traditionally, dependently typed languages have been based on constructive type theories, where the connection between proofs and programs is based on the Curry-Howard correspondence. This connection comes at a price, however, as it is necessary for the languages to be normalizing to preserve logical soundness. Trellys is a call-by-value dependently typed programming language currently in development that is designed to integrate a type theory with unsound programming features, such as general recursion, Type:Type, and others. In this paper we outline one core language …
Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich
Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich
Stephanie Weirich
Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.