Computer Engineering Commons^™

Software Metrics And Dashboard, Shilpika Shilpika, George K. Thiruvathukal, Saulo Aguiar, Konstantin Läufer, Nicholas J. Hayward

George K. Thiruvathukal

Software metrics are a critical tool which provide continuous insight to products and processes and help build reliable software in mission critical environments. Using software metrics we can perform calculations that help assess the effectiveness of the underlying software or process. The two types of metrics relevant to our work is complexity metrics and in-process metrics. Complexity metrics tend to focus on intrinsic code properties like code complexity. In-process metrics focus on a higher-level view of software quality, measuring information that can provide insight into the underlying software development process.

Our aim is to develop and evaluate a metrics dashboard …

Towards Real-Time, On-Board, Hardware-Supported Sensor And Software Health Management For Unmanned Aerial Systems, Johann M. Schumann, Kristin Y. Rozier, Thomas Reinbacher, Ole J. Mengshoel, Timmy Mbaya, Corey Ippolito

Ole J Mengshoel

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

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

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

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.

Data Management In Cloud Environments: Nosql And Newsql Data Stores, Katarina Grolinger, Wilson A. Higashino, Abhinav Tiwari, Miriam Am Capretz

Wilson A Higashino

: Advances in Web technology and the proliferation of mobile devices and sensors connected to the Internet have resulted in immense processing and storage requirements. Cloud computing has emerged as a paradigm that promises to meet these requirements. This work focuses on the storage aspect of cloud computing, specifically on data management in cloud environments. Traditional relational databases were designed in a different hardware and software era and are facing challenges in meeting the performance and scale requirements of Big Data. NoSQL and NewSQL data stores present themselves as alternatives that can handle huge volume of data. Because of the …