Author

Kenneth Knowles

12 papers · 2006–2021

2006peak 2 in 20072021

Frequent co-authors

Papers

showing 1–12 of 12 RSS

Hybrid type checking

Artificial Intelligence · ACM Transactions on Programming Languages and Systems · 2010 · cited 115× · DOI ↗ · more like this ·

Traditional static type systems are effective for verifying basic interface specifications. Dynamically checked contracts support more precise specifications, but these are not checked until runtime, resulting in incomplete detection of defects. Hybrid type checking is a synthesis of these two approaches that enforces precise interface specifications, via static analysis where possible, but also via dynamic checks where necessary. This article explores the key ideas and implications of hybrid type checking, in the context of the λ-calculus extended with contract types , that is, with dependent function types and with arbitrary refinements of base types.

Sage: Hybrid Checking for Flexible Specifications

Jessica Gronski, Kenneth Knowles, Aaron Tomb +2 more

Artificial Intelligence · 2006 · cited 66× · OpenAlex ↗ · more like this ·

Software systems typically contain large APIs that are informally specified and hence easily misused. This paper presents the Sage programming language, which is designed to enforce precise interface specifications in a flexible manner. The Sage type system uses a synthesis of the type Dynamic, first-class types, and arbitrary refinement types. Since type checking for this expressive language is not statically decidable, Sage uses hybrid type checking, which extends static type checking with dynamic contract checking, automatic theorem proving, and a database of refuted subtype judgments. 1.

Watermarks in stream processing systems

Tyler Akidau, Edmon Begoli, Slava Chernyak +5 more

Signal Processing · Proceedings of the VLDB Endowment · July 2021 · cited 39× · DOI ↗ · more like this ·

Streaming data processing is an exercise in taming disorder: from oftentimes huge torrents of information, we hope to extract powerful and timely analyses. But when dealing with streaming data, the unbounded and temporally disordered nature of real-world streams introduces a critical challenge: how does one reason about the completeness of a stream that never ends? In this paper, we present a comprehensive definition and analysis of watermarks , a key tool for reasoning about temporal completeness in infinite streams. First, we describe what watermarks are and why they are important, highlighting how they address a suite of stream processing needs that are poorly served by eventually-consistent approaches: • Computing a single correct answer, as in notifications. • Reasoning about a lack of data, as in dip detection. • Performing non-incremental processing over temporal subsets of an…

One SQL to Rule Them All - an Efficient and Syntactically Idiomatic Approach to Management of Streams and Tables

Edmon Begoli, Tyler Akidau, Fabian Hueske +3 more

Computer Networks and Communications · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 18 Jun 2019 · cited 34× · DOI ↗ · more like this ·

Real-time data analysis and management are increasingly critical for today's businesses. SQL is the de facto lingua franca for these endeavors, yet support for robust streaming analysis and management with SQL remains limited. Many approaches restrict semantics to a reduced subset of features and/or require a suite of non-standard constructs. Additionally, use of event timestamps to provide native support for analyzing events according to when they actually occurred is not pervasive, and often comes with important limitations. We present a three-part proposal for integrating robust streaming into SQL, namely: (1) time-varying relations as a foundation for classical tables as well as streaming data, (2) event time semantics, (3) a limited set of optional keyword extensions to control the materialization of time-varying query results. We show how with these minimal additions it is…

Compositional reasoning and decidable checking for dependent contract types

Kenneth Knowles, Cormac Flanagan

Artificial Intelligence · 20 Jan 2009 · cited 24× · DOI ↗ · more like this ·

Simple type systems perform compositional reasoning in that the type of a term depends only on the types of its subterms, and not on their semantics. Contracts offer more expressive abstractions, but static contract checking systems typically violate those abstractions and base their reasoning directly upon the semantics of terms. Pragmatically, this noncompositionality makes the decidability of static checking unpredictable.We first show how compositional reasoning may be restored using standard type-theoretic techniques, namely existential types and subtyping. Despite its compositional nature, our type system is exact, in that the type of a term can completely capture its semantics, hence demonstrating that precision and compositionality are compatible. We then address predictability of static checking for contract types by giving a type-checking algorithm for an important class of…

Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Extended Report)

Kenneth Knowles, Aaron Tomb, Jessica Gronski +2 more

Artificial Intelligence · 2007 · cited 21× · OpenAlex ↗ · more like this ·

This paper presents Sage, a functional programming language with a rich type system that supports a broad range of typing paradigms, from dynamically-typed Scheme-like programming, to decidable ML-like types, to precise refinement types. This type system is a synthesis of three general concepts — first-class types, general refinement types, and the type Dynamic — that add expressive power in orthogonal and complementary ways. None of these concepts are statically decidable. The Sage compiler uniformly circumvents this limitation using hybrid type checking, which inserts occasional run-time casts in particularly complicated situations that cannot be statically checked. We describe a prototype implementation of Sage and preliminary experimental results showing that most or all types are enforced via static type checking — the number of compiler-inserted casts is very small or zero on all…

One SQL to Rule Them All

Edmon Begoli, Tyler Akidau, Fabian Hueske +3 more

cs.DB · 28 May 2019 · cited 7× · arXiv ↗ · more like this ·

Real-time data analysis and management are increasingly critical for today`s businesses. SQL is the de facto lingua franca for these endeavors, yet support for robust streaming analysis and management with SQL remains limited. Many approaches restrict semantics to a reduced subset of features and/or require a suite of non-standard constructs. Additionally, use of event timestamps to provide native support for analyzing events according to when they actually occurred is not pervasive, and often comes with important limitations. We present a three-part proposal for integrating robust streaming into the SQL standard, namely: (1) time-varying relations as a foundation for classical tables as well as streaming data, (2) event time semantics, (3) a limited set of optional keyword extensions to control the materialization of time-varying query results. Motivated and illustrated using examples…

Typed Faceted Values for Secure Information Flow in Haskell

Thomas H. Austin, Kenneth Knowles, Cormac Flanagan

Artificial Intelligence · 2014 · cited 3× · OpenAlex ↗ · more like this ·

When an application fails to ensure information flow security, it may leak sensitive data such as passwords, credit card numbers, or medical records. News stories of such failures abound. Austin and Flanagan [2012] introduce faceted values ‐ values that present different behavior according to the privileges of the observer ‐ as a dynamic approach to enforcing information flow policies for an untyped, imperative -calculus. We implement faceted values as a Haskell library, elucidating their relationship to types and monadic imperative programming. In contrast to previous work, our approach does not require modification to the language runtime. In addition to pure faceted values, our library supports faceted mutable reference cells, secure facetaware socket-like communication, and robust declassification.

Proving correctness of a dynamic atomicity analysis in Coq

Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles +1 more

Artificial Intelligence · 2008 · cited 2× · OpenAlex ↗ · more like this ·

Writing and reasoning about concurrent programs remains notoriously difficult despite the proliferation of type systems, static analyses, and dynamic analyses targeting concurrent programs. There are examples of verified developments for concurrent languages and programs (Chou and Peled 1996; Affeldt and Kobayashi 2004; Feng et al. 2007; Hobor et al. 2008) but most analyses – especially dynamic analyses – have not been subjected to mechanical rigor. We report on our partial mechanization in Coq of the recentlyreleased Velodrome dynamic atomicity checker (Flanagan et al. 2008). Velodrome examines a trace of a program to ensure that its atomic blocks are serializable. We specify the Velodrome analysis using a multi-threaded operational semantics with a collection of invariants relating the state of the analysis data structures to properties of the program trace. On top of an…

Executable Refinement Types

Kenneth Knowles

cs.PL · 13 Mar 2014 · cited 1× · arXiv ↗ · more like this ·

This dissertation introduces executable refinement types, which refine structural types by semi-decidable predicates, and establishes their metatheory and accompanying implementation techniques. These results are useful for undecidable type systems in general. Particular contributions include: (1) Type soundness and a logical relation for extensional equivalence for executable refinement types (though type checking is undecidable); (2) hybrid type checking for executable refinement types, which blends static and dynamic checks in a novel way, in some sense performing better statically than any decidable approximation; (3) a type reconstruction algorithm - reconstruction is decidable even though type checking is not, when suitably redefined to apply to undecidable type systems; (4) a novel use of existential types with dependent types to ensure that the language of logical formulae is…

Compositional and Decidable Checking for Dependent Contract Types

Kenneth Knowles, Cormac Flanagan

Artificial Intelligence · 2008 · cited 1× · OpenAlex ↗ · more like this ·

Simple type systems perform compositional reasoning in that the type of a term depends only on the types of its subterms, and not on their semantics. Contracts offer more expressive abstractions, but static contract checking systems typically violate those abstractions and base their reasoning directly upon the semantics of terms. Pragmatically, this noncompositionality makes the decidability of static checking unpredictable. We first show how compositional reasoning may be restored using standard type-theoretic techniques, namely existential types and subtyping. Despite its compositional nature, our type system is exact, in that the type of a term can completely capture its semantics, hence demonstrating that precision and compositionality are compatible. We then address predictability of static checking for contract types by giving a type-checking algorithm for an important class of…

Explicit names without -equivalence: Simple type soundness for a CEK semantics.

Kenneth Knowles, Cormac Flanagan

Artificial Intelligence · 2007 · cited 0× · OpenAlex ↗ · more like this ·

Motivation Proofs of metatheoretical properties of type systems using current techniques are notorious for straightforward but tedious inductions involving many subcases, encouraging proof elision. Ironically, as type systems are used for more complex languages and analyses, their published proofs get smaller. Today, we can expect the published soundness proof of a type system to look something like this: Proof. Straightforward induction over the derivation. Proof assistants have the potential to aid programming language researchers in writing, checking, and even typesetting correct proofs. But eectively mapping handwritten proofs to a formal system can be unpredictable. While very simple proofs may be discharged automatically by proof search, at a very moderate level of complexity mechanized proofs can become much harder than their informal counterparts. The diculty of mechanizing…