Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logic theory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the λ-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.

Advanced Persistent Threats (APTs) are sophisticated, targeted cyberattacks designed to gain unauthorized access to systems and remain undetected for extended periods. To evade detection, APT cyberattacks deceive defense layers with breaches and exploits, thereby complicating exposure by traditional anomaly detection-based security methods. The challenge of detecting APTs with machine learning is compounded by the rarity of relevant datasets and the significant imbalance in the data, which makes the detection process highly burdensome. We present AE-APT, a deep learning-based tool for APT detection that features a family of AutoEncoder methods ranging from a basic one to a Transformer-based one. We evaluated our tool on a suite of provenance trace databases produced by the DARPA Transparent Computing program, where APT-like attacks constitute as little as 0.004% of the data. The datasets span multiple operating systems, including Android, Linux, BSD, and Windows, and cover two attack scenarios. The outcomes showed that AE-APT has significantly higher detection rates compared to its competitors, indicating superior performance in detecting and ranking anomalies. Data and code: https://github.com/ae-apt/AE-APT.

Abstract Data integration is a classical problem in databases, typically decomposed into schema matching, entity matching and data fusion. To solve the latter, it is mostly assumed that ground truth can be determined. However, in general, the data gathering processes in the different sources are imperfect and cannot provide an accurate merging of values. Thus, in the absence of ways to determine ground truth, it is important to at least quantify how far from being internally consistent a dataset is. Hence, we propose definitions of concordant data and define a discordance metric as a way of measuring disagreement to improve decision-making based on trustworthiness. We define the discord measurement problem of numerical attributes in which given a set of uncertain raw observations or aggregate results (such as case/hospitalization/death data relevant to COVID-19) and information on the alignment of different conceptualizations of the same reality (e.g., granularities or units), we wish to assess whether the different sources are concordant, or if not, use the discordance metric to quantify how discordant they are. We also define a set of algebraic operators to describe the alignments of different data sources with correctness guarantees, together with two alternative relational database implementations that reduce the problem to linear or quadratic programming. These are evaluated against both COVID-19 and synthetic data, and our experimental results show that discordance measurement can be performed efficiently in realistic situations.

Modern applications often manage time-varying data. Despite decades of research on temporal databases, which culminated in the addition of temporal data operations into the SQL:2011 standard, temporal data query and manipulation operations are unavailable in most mainstream database management systems, leaving developers with the unenviable task of implementing such functionality from scratch.

We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the Gabbay-Pitts nominal approach. Matching logic is the foundation of the framework, used to specify programming languages and automatically derive associated tools (compilers, debuggers, model checkers, program verifiers). Matching logic does not include a primitive notion of name binding, though binding operators can be represented via an encoding that internalises the graph of a function from bound names to expressions containing bound names. This approach is sufficient to represent computations involving binding operators, but has not been reconciled with support for inductive reasoning over syntax with binding (e.g., reasoning over λ-terms). Nominal logic is a formal system for reasoning about names and binding, which provides well-behaved and powerful principles for inductive reasoning over syntax with binding, and NML inherits these principles. We discuss design alternatives for the syntax and the semantics of NML, prove meta-theoretical properties and give examples to illustrate its expressive power. In particular, we show how induction principles for λ-terms (α-structural induction) can be defined and used to prove standard properties of the λ-calculus.

SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL's semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.

Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about the nested relational calculus, stating that its queries can be algorithmically translated to SQL, as long as their result type is a flat relation. Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However, the translation of higher-order relational queries to SQL relies on a rewrite system for which no strong normalization proof has been published: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the $\top\top$-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also show how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.

FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Rémy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

Abstract Language-integrated query based on comprehension syntax is a powerful technique for safe database programming, and provides a basis for advanced techniques such as query shredding or query flattening that allow efficient programming with complex nested collections. However, the foundations of these techniques are lacking: although SQL, the most widely-used database query language, supports heterogeneous queries that mix set and multiset semantics, these important capabilities are not supported by known correctness results or implementations that assume homogeneous collections. In this paper we study language-integrated query for a heterogeneous query language $$\mathcal {NRC}_{\lambda }( Set,Bag )$$ NRC λ ( S e t , B a g ) that combines set and multiset constructs. We show how to normalize and translate queries to SQL, and develop a novel approach to querying heterogeneous nested collections, based on the insight that “local” query subexpressions that calculate nested subcollections can be “lifted” to the top level analogously to lambda-lifting for local function definitions.

Advanced persistent threats (APT) are stealthy cyber-attacks that are aimed at stealing valuable information from target organizations and tend to extend in time. Blocking all APTs is impossible, security experts caution, hence the importance of research on early detection and damage limitation. Whole-system provenance-tracking and provenance trace mining are considered promising as they can help find causal relationships between activities and flag suspicious event sequences as they occur. We introduce an unsupervised method that exploits OS-independent features reflecting process activity to detect realistic APT-like attacks from provenance traces. Anomalous processes are ranked using both frequent and rare event associations learned from traces. Results are then presented as implications which, since interpretable, help leverage causality in explaining the detected anomalies. When evaluated on Transparent Computing program datasets (DARPA), our method outperformed competing approaches.

The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.

Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal semantics as a first step. This can take months or years of effort. Can we (at least partially) automate this process? Though desirable, automatically reverse-engineering semantics rules from an implementation is very challenging, as found by Krishnamurthi, Lerner and Elberty. In this paper, we highlight that scaling methods with the size of the language is very difficult due to state space explosion, so we propose to learn semantics incrementally. We give a formalisation of Krishnamurthi et al.'s desugaring learning framework in order to clarify the assumptions necessary for an incremental learning algorithm to be feasible. We show that this reformulation allows us to extend the search space and express rules that Krishnamurthi et al. described as challenging, while still retaining feasibility. We evaluate enumerative synthesis as a baseline algorithm, and demonstrate that, with our reformulation of the problem, it is possible to learn correct desugaring rules for the example source and core languages proposed by Krishnamurthi et al., in most cases identical to the intended rules. In addition, with user guidance, our system was able to synthesize rules for desugaring list comprehensions and try/catch/finally constructs.

Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However there is no published proof of the central strong normalization property for higher-order nested relational queries: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the ⊤⊤-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also sketch how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.

ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types.

System level provenance is of widespread interest for applications such as security enforcement and information protection. However, testing the correctness or completeness of provenance capture tools is challenging and currently done manually. In some cases there is not even a clear consensus about what behavior is correct. We present an automated tool, ProvMark, that uses an existing provenance system as a black box and reliably identifies the provenance graph structure recorded for a given activity, by a reduction to subgraph isomorphism problems handled by an external solver. ProvMark is a beginning step in the much needed area of testing and comparing the expressiveness of provenance systems. We demonstrate ProvMark's usefuless in comparing three capture systems with different architectures and distinct design philosophies.

Ideas from programming languages play an important role in a range of advanced applications of databases, in database system implementation, distributed programming (MapReduce), streaming computation, and high-performance (GPU/multicore) computation. This creative research area is broadening into a subfield of data-centric computation. Although the interaction of databases and programming has a long history (the 16th biennial Database Programming Languages symposium was held in 2017), there has been a recent renewal of interest and broadening of programming language techniques for dealing with data from several quarters in the last few years, including workshops at Microsoft Research (RADICAL 2010), ICFP (XLDI 2012), POPL (DDFP 2013, DCM 2014) and a Dagstuhl Seminar on Programming Languages for Big Data (December 2014). This special issue recognises and encourages the publication of mature research contributions in this area.

We present a formalisation in Agda of the theory of concurrent transitions, residuation and causal equivalence of traces for the π-calculus. Our formalisation employs de Bruijn indices and dependently typed syntax, and aligns the ‘proved transitions’ proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agda's representation of the labelled transition relation. Our main contributions are proofs of the ‘diamond lemma’ for the residuals of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions. In the π-calculus, transitions represent propagating binders whenever their actions involve bound names. To accommodate these cases, we require a more general diamond lemma where the target states of equivalent traces are no longer identical, but are related by abraidingthat rewires the bound and free names to reflect the particular interleaving of events involving binders. Our approach may be useful for modelling concurrency in other languages where transitions carry meta-data sensitive to particular interleavings, such as dynamically allocated memory addresses.

Lenses are a popular approach to bidirectional transformations, a generalisation of the view update problem in databases, in which we wish to make changes to source tables to effect a desired change on a view . However, perhaps surprisingly, lenses have seldom actually been used to implement updatable views in databases. Bohannon, Pierce and Vaughan proposed an approach to updatable views called relational lenses , but to the best of our knowledge this proposal has not been implemented or evaluated to date. We propose incremental relational lenses , that equip relational lenses with change-propagating semantics that map small changes to the view to (potentially) small changes to the source tables. We also present a language-integrated implementation of relational lenses and a detailed experimental evaluation, showing orders of magnitude improvement over the non-incremental approach. Our work shows that relational lenses can be used to support expressive and efficient view updates at the language level, without relying on updatable view support from the underlying database.

Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called $λ^h$ that supports auditing. However, $λ^h$ is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of $λ^h$ is inconsistent. We introduce a new calculus $λ^{hc}$ that is simpler than $λ^h$, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.

Puppet is a popular declarative framework for specifying and managing complex system configurations. The Puppet framework includes a domain-specific language with several advanced features inspired by object-oriented programming, including user-defined resource types, `classes’ with a form of inheritance, and dependency management. Like most real-world languages, the language has evolved in an ad hoc fashion, resulting in a design with numerous features, some of which are complex, hard to understand, and difficult to use correctly. We present an operational semantics for $\mu$Puppet, a representative subset of the Puppet language that covers the distinctive features of Puppet, while excluding features that are either deprecated or work-in-progress. Formalizing the semantics sheds light on difficult parts of the language, identifies opportunities for future improvements, and provides a foundation for future analysis or debugging techniques, such as static typechecking or provenance tracking. Our semantics leads straightforwardly to a reference implementation in Haskell. We also discuss some of Puppet’s idiosyncrasies, particularly its handling of classes and scope, and present an initial corpus of test cases supported by our formal semantics.

Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work, where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.

Across many domains, there is a need to trace how data has been created, manipulated, and disseminated.This has led to strong recent interest in technology for modelling and reasoning about provenance.Provenance is information about the entities, activities, and people involved in producing a piece of data or thing, which can be used to form assessments about its quality, reliability, or trustworthiness.It is itself data, commonly represented as a directed acyclic graph linking these elements (entities, activities, and agents) to the earlier elements that influenced them.Provenance is becoming a key Internet technology, and the World Wide Web Consortium has standardised PROV as a representation for exchanging provenance on the (Semantic) Web.It is also important in a number of other settings to address the problems that arise in a distributed, internetworked world: for example, the need to document the sources of information in order to establish their trustworthiness, and the need to secure critical systems from attackers who can, thanks to the Internet, be located anywhere in the world.Access to provenance information underlies our ability to interpret and to judge the reliability of data, whether on the Web, in databases, or within and between applications.Despite much recent progress, it is still uncommon for people or software to have access to the provenance of online data.The formal requirements for provenance, including issues such as correctness, completeness, and security of provenance, are not yet fully understood.The question of what is semantically useful provenance and how to capture it is still open, as are benchmarks that could be used to measure the performance of proposed systems.Moreover, as the patterns of use on the Internet change, with greater prevalence of crowdsourcing of information and services, virtualisation of applications in clouds, location-aware streaming, and so on, both the technological and social requirements on provenance are evolving.

Abstract The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has attracted comparatively little attention. In this article, we present αCheck, a bounded model checker for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based onnegation-as-failureand one based onnegation elimination, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.

We offer a lattice-theoretic account of the problem of dynamic slicing for pi-calculus, building on prior work in the sequential setting. For any particular run of a concurrent program, we exhibit a Galois connection relating forward and backward slices of the initial and terminal configurations. We prove that, up to lattice isomorphism, the same Galois connection arises for any causally equivalent execution, allowing an efficient concurrent implementation of slicing via a standard interleaving semantics. Our approach has been formalised in the dependently-typed programming language Agda.

Provenance, or information about the origin or derivation of data, is important for assessing the trustworthiness of data and identifying and correcting mistakes. Most prior implementations of data provenance have involved heavyweight modifications to database systems and little attention has been paid to how the provenance data can be used outside such a system. We present extensions to the Links programming language that build on its support for language-integrated query to support provenance queries by rewriting and normalizing monadic comprehensions and extending the type system to distinguish provenance metadata from normal data. The main contribution of this paper is to show that the two most common forms of provenance can be implemented efficiently and used safely as a programming language feature with no changes to the database system.

Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new-quantifier are much simpler than in previous attempts. We also prove several structural and metatheoretic properties, including cut-elimination, consistency and equivalence to Pitts' axiomatization of nominal logic.

The prov family of documents are the final output of the World Wide Web Consortium Provenance Working Group, chartered to specify a representation of provenance to facilitate its exchange over the Web. This article reflects upon the key requirements, guiding principles, and design decisions that influenced the prov family of documents. A broad range of requirements were found, relating to the key concepts necessary for describing provenance, such as resources, activities, agents and events, and to balancing prov’s ease of use with the facility to check its validity. By this retrospective requirement analysis, the article aims to provide some insights into how prov turned out as it did and why. Benefits of this insight include better inter-operability, a roadmap for alternate investigations and improvements, and solid foundations for future standardization activities.

Language-integrated query techniques have been explored in a number of different language designs. We consider two different, type-safe approaches employed by Links and F#. Both approaches provide rich dynamic query generation capabilities, and thus amount to a form of heterogeneous staged computation, but to date there has been no formal investigation of their relative expressiveness. We present two core calculi Eff and Quot, respectively capturing the essential aspects of language-integrated querying using effects in Links and quotation in LINQ. We show via translations from Eff to Quot and back that the two approaches are equivalent in expressiveness. Based on the translation from Eff to Quot, we extend a simple Links compiler to handle queries.

Provenance for database queries or scientific workflows is often motivated as providing explanation, increasing understanding of the underlying data sources and processes used to compute the query, and reproducibility, the capability to recompute the results on different inputs, possibly specialized to a part of the output. Many provenance systems claim to provide such capabilities; however, most lack formal definitions or guarantees of these properties, while others provide formal guarantees only for relatively limited classes of changes. Building on recent work on provenance traces and slicing for functional programming languages, we introduce a detailed tracing model of provenance for multiset-valued Nested Relational Calculus, define trace slicing algorithms that extract subtraces needed to explain or recompute specific parts of the output, and define query slicing and differencing techniques that support explanation. We state and prove correctness properties for these techniques and present a proof-of-concept implementation in Haskell.

Nested relational query languages have been explored extensively, and underlie industrial language-integrated query systems such as Microsoft's LINQ. However, relational databases do not natively support nested collections in query results. This can lead to major performance problems: if programmers write queries that yield nested results, then such systems typically either fail or generate a large number of queries. We present a new approach to query shredding, which converts a query returning nested data to a fixed number of SQL queries. Our approach, in contrast to prior work, handles multiset semantics, and generates an idiomatic SQL:1999 query directly from a normal form for nested queries. We provide a detailed description of our translation and present experiments showing that it offers comparable or better performance than a recent alternative approach on a range of examples.

Provenance, a form of structured metadata designed to record the origin or source of information, can be instrumental in deciding whether information is to be trusted, how it can be integrated with other diverse information sources, and how to establish attribution of information to authors throughout its history. The PROV set of specifications, produced by the World Wide Web Consortium (W3C), is designed to promote the publication of provenance information on the Web, and offers a basis for interoperability across diverse provenance management systems. The PROV provenance model is deliberately generic and domain-agnostic, but extension mechanisms are available and can be exploited for modelling specific domains. This tutorial provides an account of these specifications. Starting from intuitive and informal examples that present idiomatic provenance patterns, it progressively introduces the relational model of provenance along with the constraints model for validation of provenance documents, and concludes with example applications that show the extension points in use.

Language-integrated query is receiving renewed attention, in part because of its support through Microsoft's LINQ framework. We present a practical theory of language-integrated query based on quotation and normalisation of quoted terms. Our technique supports join queries, abstraction over values and predicates, composition of queries, dynamic generation of queries, and queries with nested intermediate data. Higher-order features prove useful even for constructing first-order queries. We prove a theorem characterising when a host query is guaranteed to generate a single SQL query. We present experimental results confirming our technique works, even in situations where Microsoft's LINQ framework either fails to produce an SQL query or, in one case, produces an avalanche of SQL queries.

Provenance is an increasing concern due to the ongoing revolution in sharing and processing scientific data on the Web and in other computer systems. It is proposed that many computer systems will need to become provenance-aware in order to provide satisfactory accountability, reproducibility, and trust for scientific or other high-value data. To date, there is not a consensus concerning appropriate formal models or security properties for provenance. In previous work, we introduced a formal framework for provenance security and proposed formal definitions of properties called disclosure and obfuscation. In this article, we study refined notions of positive and negative disclosure and obfuscation in a concrete setting, that of a general-purpose programing language. Previous models of provenance have focused on special-purpose languages such as workflows and database queries. We consider a higher-order, functional language with sums, products, and recursive types and functions, and equip it with a tracing semantics in which traces themselves can be replayed as computations. We present an annotation-propagation framework that supports many provenance views over traces, including standard forms of provenance studied previously. We investigate some relationships among provenance views and develop some partial solutions to the disclosure and obfuscation problems, including correct algorithms for disclosure and positive obfuscation based on trace slicing.

In “Forward Node-Selecting Queries over Trees,” Olteanu [2007] gives three rewriting systems for eliminating reverse XPath axis steps from node-selecting queries over trees, together with arguments for their correctness and termination for a large class of input graphs, including cyclic ones. These proofs are valid for tree or acyclic formulas, but two of the rewrite systems ( TRS 2 and TRS 3 ) do not terminate on cyclic graphs; that is, there are infinite rewrite sequences that never yield a normal form. We investigate the reasons why the termination arguments do not work for general cyclic formulas, and develop alternative algorithms that can be used instead. We prove that TRS 2 is weakly normalizing, while TRS 3 is not weakly normalizing, but it can be extended to a weakly normalizing system TRS 3 ○ . The algorithms and proof techniques illustrate unforeseen subtleties in the handling of cyclic queries.

We present techniques that enable higher-order functional computations to "explain" their work by answering questions about how parts of their output were calculated. As explanations, we consider the traditional notion of program slices, which we show can be inadequate, and propose a new notion: trace slices. We present techniques for specifying flexible and rich slicing criteria based on partial expressions, parts of which have been replaced by holes.

The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 27–29, 2010 in Baltimore, Maryland. After the conference, the programme committee, chaired by Stephanie Weirich, selected several outstanding papers and invited their authors to submit to this special issue of Journal of Functional Programming . Umut A. Acar and James Cheney acted as editors for these submissions. This issue includes the seven accepted papers, each of which provides substantial new material beyond the original conference version. The selected papers reflect a consensus by the program committee that ICFP 2010 had a number of strong papers that link core functional programming ideas with other areas, such as multicore, embedded systems, and data compression.

Provenance, or information about the origin, derivation, or history of data, is becoming an important topic especially for shared scientific or public data on the Web. It clearly has implications on security (and vice versa) yet these implications are not well-understood. A great deal of work has focused on mechanisms for recording, managing or using some kind of provenance information, but relatively little progress has been made on foundational models that define provenance and relate it to security goals such as availability, confidentiality or privacy. We argue that such foundations are essential to making meaningful progress on these problems and should be developed. In this paper, we outline a formal model of provenance, propose formalizations of security properties for provenance such as disclosure and obfuscation, and explore their implications in domains based on automata, database queries and workflow provenance graphs.

We investigate the satisfiability problem for conjunctions of constraints over ordered, unranked trees, including child, descendant, following-sibling, root, leaf, and first/last child constraints. We introduce new, symbolic approaches based on graph transformations, which simplify and check the consistency of a problem first, and delay blind search as long as possible. We prove correctness and termination for these algorithms. We also analyze the complexity of important special cases: binary and κ-ary intersection of certain classes of XPath expressions. Our main complexity result is that binary intersection (for positive, simple navigational XPath over all axes) is tractable for expressions with a bounded number of changes in direction in the path, which is typically small.

Wikis have proved enormously successful as a means to collaborate in the creation and publication of textual information. At the same time, a large number of curated databases have been developed through collaboration for the dissemination of structured data in specific domains, particularly bioinformatics. We demonstrate a general-purpose platform for collaborative data management, DBWiki, designed to achieve the best of both worlds. Our system not only facilitates the collaborative creation of a database; it also provides features not usually provided by database technology such as versioning, provenance tracking, citability, and annotation. In our demonstration we will show how DBWiki makes it easy to create, correct, discuss and query structured data, placing more power in the hands of users while managing tedious details of data curation automatically.

Provenance is information recording the source, derivation or history of some information. Provenance tracking has been studied in a variety of settings, particularly database management systems. However, although many candidate definitions of provenance have been proposed, the mathematical or semantic foundations of data provenance have received comparatively little attention. In this paper, we argue that dependency analysis techniques familiar from program analysis and program slicing provide a formal foundation for forms of provenance that are intended to show how (part of) the output of a query depends on (parts of) its input. We introduce a semantic characterisation of such dependency provenance for a core database query language, show that minimal dependency provenance is not computable, and provide dynamic and static approximation techniques. We also discuss preliminary implementation experience with using dependency provenance to compute data slices, or summaries of the parts of the input relevant to a given part of the output.

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the Nominal Datatype Package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. We also formally derive a version of the type checking algorithm from which Isabelle/HOL can generate executable code. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.

Independence analysis is the problem of determining whether an update affects the result of a query, e.g. a constraint or materialized view. We develop a new, modular framework for static independence analysis that decomposes the problem into two orthogonal subproblems: approximating the destabilizer , that is, a finite representation of the set of updates that can change the result of the query, and testing whether the update and destabilizer overlap via an intersection analysis. Focusing on XML queries as the view language and the XQuery Update Facility as the update language, we present a syntactic query rewriting algorithm for translating queries to destabilizers, and show that intersection checking can be reduced to satisfiability problems for which efficient checkers already exist. We present an implementation based on an expressive tree satisfiability checker and a Satisfiability Modulo Order package, and give experiments confirming that the resulting analysis is both fast and effective.

Shin et al [19] and McKay et al [15] previously applied tree compression and semantics-based simplification to study the distribution of building blocks in evolving Genetic Programming populations. However their method could only give static estimates of the degree of repetition of building blocks in one generation at a time, supplying no information about the flow of building blocks between generations. Here, we use a state-of-the-art tree compression algorithm, xmlppm, to estimate the extent to which frequent building blocks from one generation are still in use in a later generation. While they compared the behaviour of different GP algorithms on one specific problem -- a simple symbolic regression problem -- we extend the analysis to a more complex problem, a symbolic regression problem to find a Fourier approximation to a sawtooth wave, and to a Boolean domain, odd parity.

Query-update independence analysis is the problem of determining whether an update affects the results of a query. Query-update independence is useful for avoiding recomputation of materialized views and may have applications to access control and concurrency control. This paper develops static analysis techniques for query-update independence problems involving core XQuery queries and updates with a snapshot semantics (based on the W3C XQuery Update Facility proposal). Our approach takes advantage of schema information, in contrast to previous work on this problem. We formalize our approach, sketch a proof of correctness, and report on the performance and accuracy of our implementation.

XML access control policies involving updates may contain security flaws, here called inconsistencies, in which a forbidden operation may be simulated by performing a sequence of allowed operations. ACCOn implements i) consistency checking algorithms that examine whether a write-access control policy defined over a DTD is inconsistent and ii) repair algorithms that propose repairs to an inconsistent policy to obtain a consistent one.

XML database query languages have been studied extensively, but XML database updates have received relatively little attention, and pose many challenges to language design. We are developing an XML update language called FLUX, which stands for FunctionaL Updates for XML, drawing upon ideas from functional programming languages. In prior work, we have introduced a core language for FLUX with a clear operational semantics and a sound, decidable static type system based on regular expression types.

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the nominal datatype package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.

Curated databases are databases that are populated and updated with a great deal of human effort. Most reference works that one traditionally found on the reference shelves of libraries -- dictionaries, encyclopedias, gazetteers etc. -- are now curated databases. Since it is now easy to publish databases on the web, there has been an explosion in the number of new curated databases used in scientific research. The value of curated databases lies in the organization and the quality of the data they contain. Like the paper reference works they have replaced, they usually represent the efforts of a dedicated group of people to produce a definitive description of some subject area. Curated databases present a number of challenges for database research. The topics of annotation, provenance, and citation are central, because curated databases are heavily cross-referenced with, and include data from, other databases, and much of the work of a curator is annotating existing data. Evolution of structure is important because these databases often evolve from semistructured representations, and because they have to accommodate new scientific discoveries. Much of the work in these areas is in its infancy, but it is beginning to provide suggest new research for both theory and practice. We discuss some of this research and emphasize the need to find appropriate models of the processes associated with curated databases.

Information describing the origin of data, generally referred to as provenance , is important in scientific and curated databases where it is the basis for the trust one puts in their contents. Since such databases are constructed using operations of both query and update languages, it is of paramount importance to describe the effect of these languages on provenance. In this article we study provenance for query and update languages that are closely related to SQL, and compare two ways in which they can manipulate provenance so that elements of the input are rearranged to elements of the output: implicit provenance , where a query or update only provides the rearranged output, and provenance is provided implicitly by a default provenance semantics; and explicit provenance , where a query or update provides both the output and the description of the provenance of each component of the output. Although explicit provenance is in general more expressive, we show that the classes of implicit provenance operations expressible by query and update languages correspond to natural semantic subclasses of the explicit provenance queries. One of the consequences of this study is that provenance separates the expressive power of query and update languages. The model is also relevant to annotation propagation schemes in which annotations on the input to a query or update have to be transferred to the output or vice versa.

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.

The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has received comparatively little attention. In this paper, we consider the problem of bounded model-checking for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on negation-as-failure and one based on negation elimination, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.

Large XML data files, or XML databases, are now a common way to distribute scientific and bibliographic data, and storing such data efficiently is an important concern. A number of approaches to XML compression have been proposed in the last five years. The most competitive approaches employ one or more statistical text compressors based on PPM or arithmetic coding in which some of the context is provided by the XML document structure. The purpose of this paper is to investigate the relationship between the extant proposals in more detail. We review the two main statistical modeling approaches proposed so far, and evaluate their performance on two representative XML databases. Our main finding is that while a recently-proposed multiple-model approach can provide better overall compression for large databases, it uses much more memory and converges more slowly than an older single-model approach.

Curated databases in bioinformatics and other disciplines are the result of a great deal of manual annotation, correction and transfer of data from other sources. Provenance information concerning the creation, attribution, or version history of such data is crucial for assessing its integrity and scientific value. General purpose database systems provide little support for tracking provenance, especially when data moves among databases. This paper investigates general-purpose techniques for recording provenance for data that is copied among databases. We describe an approach in which we track the user's actions while browsing source databases and copying data into a curated database, in order to record the user's actions in a convenient, queryable form. We present an implementation of this technique and use it to evaluate the feasibility of database support for provenance management. Our experiments show that although the overhead of a naive approach is fairly high, it can be decreased to an acceptable level using simple optimizations.

Abstract Nominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations:name-swapping andfreshness. It relies on two important principles:equivariance(validity is preserved by name-swapping), andfresh name generation(“new” or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory:finite-support modelsin which each value can depend on only finitely many names. Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete:ideal-supportedmodels in which the supports of values are elements of a proper ideal on the set of names. We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalizeuniversaltheories tonominal-universaltheories and prove that each such theory has an Herbrand model.

Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N- (or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called fresh logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret FO/spl lambda//spl nabla/, another logic with a self-dual quantifier, within FL.

The recent years have seen a number of proposals for extending statically typed languages by dynamics or generics. Most proposals --- if not all --- require significant extensions to the underlying language. In this paper we show that this need not be the case. We propose a particularly lightweight extension that supports both dynamics and generics. Furthermore, the two features are smoothly integrated: dynamic values, for instance, can be passed to generic functions. Our proposal makes do with a standard Hindley-Milner type system augmented by existential types. Building upon these ideas we have implemented a small library that is readily usable both with Hugs and with the Glasgow Haskell compiler.

Cyclone is a type-safe programming language derived from C. The primary design goal of Cyclone is to let programmers control data representation and memory management without sacrificing type-safety. In this paper, we focus on the region-based memory management of Cyclone and its static typing discipline. The design incorporates several advancements, including support for region subtyping and a coherent integration with stack allocation and a garbage collector. To support separate compilation, Cyclone requires programmers to write some explicit region annotations, but a combination of default annotations, local type inference, and a novel treatment of region effects reduces this burden. As a result, we integrate C idioms in a region-based framework. In our experience, porting legacy C to Cyclone has required altering about 8% of the code; of the changes, only 6% (of the 8%) were region annotations.

We established a working Extensible Markup Language (XML) compression benchmark based on text compression, and found that bzip2 compresses XML best, albeit more slowly than gzip. Our experiments verified that T/sub XMILL/ speeds up and improves compression using gzip and bounded-context PPM by up to 15%, but found that it worsens the compression for bzip2 and PPM. We describe alternative approaches to XML compression that illustrate other tradeoffs between speed and effectiveness. We describe experiments using several text compressors and XMILL to compress a variety of XML documents. Using these as a benchmark, we describe our two main results: an online binary encoding for XML called Encoded SAX (ESAX) that compresses better and faster than existing methods; and an online, adaptive, XML-conscious encoding based on prediction by partial match (PPM) called multiplexed hierarchical modeling (MHM) that compresses up to 35 % better than any existing method but is fairly slow.

Summary form only given. Computing systems frequently deal with symbolic tree data structures, which are also known as terms in universal algebra and logic. Our goal is to develop universal, effective and efficient term compression techniques superior to specialized or universal compression techniques currently available. Our approach is to use knowledge of term structure to build accurate universal statistical models of terms. These models can compress terms faster or more effectively than comparable sequential methods. We present two statistical term models that are related to Markov random fields over trees. These models gather statistical information about parent-child symbol relationships in terms. Huffman or arithmetic codes generated from these probability estimates are used to encode the terms. In the first model, a symbol's value is predicted by the value of its parent symbol alone. Thus, in compressing a subterm of the form t+u, the +operator would be used to select a specialized code for the root symbols of subterms t and u. The second model also uses the symbol's argument position as a predictor. For example, in compressing t+u, we would make different probability estimates for the first and second arguments, and use one code to encode the first children of + and another code for the second children. It might be the case that t+1 (but not 1+t) occurs frequently for many different terms t, in which case we could give 1 a shorter code as the second child of +. We have not achieved our goal of improved term compression, but we believe that more sophisticated and more effective techniques remain to be investigated. For example one improvement would be to make a term version of PPM in which contexts are ancestor symbols in the term rather than predecessors in a sequence. Our implementation could be viewed as a first step in that direction.