Open Access. Powered by Scholars. Published by Universities.®
- Keyword
- File Type
Articles 1 - 5 of 5
Full-Text Articles in Computer Engineering
Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract, Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee
Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract, Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee
Stephanie Weirich
No abstract provided.
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 …
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 …
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 …
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.