Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi

The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek & Taha (2006) and its underlying cast calculus. For example, Wadler and Findler (2009) added blame tracking, Siek et al. (2009) investigated alternate cast evaluation strategies, and Herman et al. (2010) replaced casts with coercions for space efficiency. The meta-theory for the GTLC has also expanded beyond type safety to include blame safety (Tobin-Hochstadt & Felleisen, 2006), space consumption (Herman et al., 2010), and the gradual guarantees (Siek et al., 2015). These results have been proven for some variations of the GTLC but not others. Furthermore, researchers continue to develop variations on the GTLC, but establishing all of the meta-theory for new variations is time-consuming. This article identifies abstractions that capture similarities between many cast calculi in the form of two parameterized cast calculi, one for the purposes of language specification and the other to guide space-efficient implementations. The article then develops reusable meta-theory for these two calculi, proving type safety, blame safety, the gradual guarantees, and space consumption. Finally, the article instantiates this meta-theory for eight cast calculi including five from the literature and three new calculi. All of these definitions and theorems, including the two parameterized calculi, the reusable meta-theory, and the eight instantiations, are mechanized in Agda making extensive use of module parameters and dependent records to define the abstractions.

XcalableMP Programming Model and Language

XcalableMP (XMP) is a directive-based language extension of Fortran and C for distributed-memory parallel computers, and can be classified as a partitioned global address space (PGAS) language. One of the remarkable characteristics of XMP is that it supports both global-view and local-view parallel programming. This chapter describes the programming model and language specification of XMP.

Active Rules in a Graph Database Environment

With the rapid growth of data nowadays, new types of database systems are emerging in order to handle big data, known as NoSQL databases. One type of NoSQL databases is graph database, which uses the graph model to present data and the relationships among data. Existing graph database systems are passive compared to traditional relational database systems that allow automatic event handling through active rules. This paper describes our approach of incorporating active rules into graph databases, allowing users to specify business logic in a declarative manner. The active system has been built on top of a passive graph database to react to events automatically. Our focus is to specify business rules declaratively rather than enforce integrity constraint using rules. Our system consists of a language framework and an execution model. Language specification will further be illustrated by on a motivating example that shows the use of rules in an application context. The paper also describes the design and implementation of the execution model in detail.