Explosive growth in DRAM capacities and the emergence of language-integrated query enable a new class of managed applications that perform complex query processing on huge volumes of data stored as collections of objects in the memory space of the application. While more flexible in terms of schema design and application development, this approach typically experiences sub-par query execution performance when compared to specialized systems like DBMS. To address this issue, we propose self-managed collections, which utilize off-heap memory management and dynamic query compilation to improve the performance of querying managed data through language-integrated query. We evaluate self-managed collections using both microbenchmarks and enumeration-heavy queries from the TPC-H business intelligence benchmark. Our results show that self-managed collections outperform ordinary managed collections in both query processing and memory management by up to an order of magnitude and even outperform an optimized in memory columnar database system for the vast majority of queries.

Current proposals for adding gradual typing to JavaScript, such as Closure, TypeScript and Dart, forgo soundness to deal with issues of scale, code reuse, and popular programming patterns. We show how to address these issues in practice while retaining soundness. We design and implement a new gradual type system, prototyped for expediency as a 'Safe' compilation mode for TypeScript. Our compiler achieves soundness by enforcing stricter static checks and embedding residual runtime checks in compiled code. It emits plain JavaScript that runs on stock virtual machines. Our main theorem is a simulation that ensures that the checks introduced by Safe TypeScript (1) catch any dynamic type error, and (2) do not alter the semantics of type-safe TypeScript code.

JavaScript's flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness for programming convenience. In this paper, we propose a gradual type system and implementation techniques that provide important safety and security guarantees.

In this paper we examine opportunities arising from the convergence of two trends in data management: in-memory database systems (imdbs), which have received renewed attention following the availability of affordable, very large main memory systems; and language-integrated query, which transparently integrates database queries with programming languages (thus addressing the famous 'impedance mismatch' problem). Language-integrated query not only gives application developers a more convenient way to query external data sources like imdbs, but also to use the same querying language to query an application's in-memory collections. The latter offers further transparency to developers as the query language and all data is represented in the data model of the host programming language. However, compared to imdbs, this additional freedom comes at a higher cost for query evaluation. Our vision is to improve in-memory query processing of application objects by introducing database technologies to managed runtimes. We focus on querying and we leverage query compilation to improve query processing on application objects. We explore different query compilation strategies and study how they improve the performance of query processing over application data. We take C# as the host programming language as it supports language-integrated query through the linq framework. Our techniques deliver significant performance improvements over the default linq implementation. Our work makes important first steps towards a future where data processing applications will commonly run on machines that can store their entire datasets in-memory, and will be written in a single programming language employing language-integrated query and imdb-inspired runtimes to provide transparent and highly efficient querying.

Abstract We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on a Satisfiability Modulo Theories solver to compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows us to show the uniqueness of normal forms for non-deterministic expressions, provide precise counterexamples when type-checking fails, detect empty types, and compute instances of types statically and at run-time.

In this paper we propose various extensions to the relational model to support similarity-based querying. We build upon the -relation model, where tuples are assigned values from an arbitrary semiring , and its associated positive relational algebra $\text{RA}^{+}_{\mathcal{K}}$ . We consider a recently proposed extension to $\text{RA}^{+}_{\mathcal{K}}$ using a monus operation on the semiring to support negative queries, and show how, surprisingly, it fails for important ‘fuzzy’ semirings. Instead, we suggest using a negation operator. We also consider the identities satisfied by the relational algebra $\text{RA}^{+}_{\mathcal{K}}$ . We show that moving from a semiring to a particular form of lattice (a De Morgan frame) yields a relational algebra that satisfies all the classical (positive) relational algebra identities. We claim that to support real-world similarity queries realistically, one must move from tuple-level annotations to attribute-level annotations. We show in detail how our De Morgan frame-based model can be extended to support attribute-level annotations and give worked examples of similarity queries in this setting.

We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types.

A number of important program rewriting scenarios can be recast as type-directed coercion insertion. These range from more theoretical applications such as coercive subtyping and supporting overloading in type theories, to more practical applications such as integrating static and dynamically typed code using gradual typing, and inlining code to enforce security policies such as access control and provenance tracking. In this paper we give a general theory of type-directed coercion insertion. We specifically explore the inherent tradeoff between expressiveness and ambiguity--the more powerful the strategy for generating coercions, the greater the possibility of several, semantically distinct rewritings for a given program. We consider increasingly powerful coercion generation strategies, work out example applications supported by the increased power (including those mentioned above), and identify the inherent ambiguity problems of each setting, along with various techniques to tame the ambiguities.

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in developing formal verification techniques, the treatment of inheritance is of paramount importance. Unfortunately, inheritance comes in a number of guises, all requiring subtle techniques.

Abstract Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example, when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically, it is provided only by ad hoc mechanisms that lack clean semantics. In this paper, we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply typed call-by-value λ calculus. To do so, we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex - time and destruct - time strategies. The latter forms the basis for a λ marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of λ marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a λ update calculus with simple primitives to provide type-safe updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

Current real-world software applications typically involve heavy use of relational and XML data and their query languages. Unfortunately object-oriented languages and database query languages are based on different semantic foundations and optimization strategies. The resulting ''ROX (Relations, Objects, XML) impedance mismatc'' makes life very difficult for developers.

This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by ensuring a property we call con-freeness. We show how con-freeness can be enforced dynamically, and how it can be approximated via a novel static analysis. This analysis can be used to assess the implications of a program's structure on future updates in order to make update success more predictable. We have implemented Proteus for C, and briefly discuss our implementation which we have tested on several well-known programs.

Many software applications today need to handle data from different data models; typically objects from the host programming language along with the relational and XML data models. The ROX impedance mismatch makes programs awkward to write and hard to maintain.The .NET Language-Integrated Query (LINQ) framework, proposed for the next release of the .NET framework, approaches this problem by defining a pattern of general-purpose standard query operators for traversal, filter, and projection. Based on this pattern, any .NET language can define special query comprehension syntax that is subsequently compiled into these standard operators (our code examples are in VB).Besides the general query operators, the LINQ framework also defines two domain specific APIs that work over XML (XLinq) and relational data (DLinq) respectively. The operators over XML use a lightweight and easy to use in-memory XML representation to provide XQuery-style expressiveness in the host programming language. The operators over relational data provide a simple OR mapping by leveraging remotable queries that are executed directly in the back-end relational store.

In this paper we address the problem of writing specifications for programs that use various forms of modularity, including procedures and Java-like classes. We build on the formalism of separation logic and introduce the new notion of an abstract predicate and, more generally, abstract predicate families. This provides a flexible mechanism for reasoning about the different forms of abstraction found in modern programming languages, such as abstract datatypes and objects. As well as demonstrating the soundness of our proof system, we illustrate its utility with a series of examples.

Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has been used for many years. Perhaps surprisingly, there is little high-level understanding or language support to help programmers write dynamic updates effectively.To bridge this gap, we present Proteus, a core calculus for dynamic software updating in C-like languages that is flexible, safe, and predictable. Proteus supports dynamic updates to functions (even active ones), to named types and to data, allowing on-line evolution to match source-code evolution as we have observed it in practice. We ensure updates are type-safe by checking for a property we call "con-freeness" for updated types t at the point of update. This means that non-updated code will not use t concretely beyond that point (concrete usages are via explicit coercions) and thus t's representation can safely change. We show how con-freeness can be enforced dynamically for a particular program state. We additionally define a novel and efficient static updateability analysis to establish con-freeness statically, and can thus automatically infer program points at which all future (well-formed) updates will be type-safe. We have implemented our analysis for C and tested it on several well-known programs.

Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value ? -calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a ?marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of ? marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a ?marsh calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

Modern database systems provide not only powerful data models but also complex query languages supporting powerful features such as the ability to create new database objects and invocation of arbitrary methods (possibly written in a third-party programming language).In this sense query languages have evolved into powerful programming languages. Surprisingly little work exists utilizing techniques from programming language research to specify and analyse these query languages. This paper provides a formal, high-level operational semantics for a complex-value OQL-like query language that can create fresh database objects, and invoke external methods. We define a type system for our query language and prove an important soundness property.We define a simple effect typing discipline to delimit the computational effects within our queries. We prove that this effect system is correct and show how it can be used to detect cases of non-determinism and to define correct query optimizations.

Researchers have recently proposed that for certain applications it is advantageous to use functional languages whose type systems are based upon linear logic: so-called linear functional languages. In this paper we develop reasoning techniques for programs in a linear functional language, linPCF , based on their operational behaviour. The principal theorem of this paper is to show that contextual equivalence of linPCF programs can be characterised coinductively. This characterisation provides a tractable method for reasoning about contextual equivalence, and is used in three ways: [bull ] A number of useful contextual equivalences between linPCF programs is given. [bull ] A notion of type isomorphism with respect to contextual equivalence, called operational isomorphism, is given. In particular the types !ϕ[otimes ]!ψ and !(ϕ&ψ) are proved to be operationally isomorphic. [bull ] A translation of non-strict PCF into linPCF is shown to be adequate, but not fully abstract, with respect to contextual equivalence.

Moggi's computational lambda calculus is a metalanguage for denotational semantics which arose from the observation that many different notions of computation have the categorical structure of a strong monad on a cartesian closed category. In this paper we show that the computational lambda calculus also arises naturally as the term calculus corresponding (by the Curry–Howard correspondence) to a novel intuitionistic modal propositional logic. We give natural deduction, sequent calculus and Hilbert-style presentations of this logic and prove strong normalisation and confluence results.