Cheney, James, Acar, Umut, Ahmed, Amal
Provenance is information about the origin, derivation, ownership, or history of an object. It has recently been studied extensively in scientific databases and other settings due to its importance...
Motivation and Vision Research Statement (2008)
Sophisticated systems such as databases and distributed (“grid ” or cyberinfrastructure) computing are becoming essential in most scientific disciplines, particularly bioinformatics. As a result,...
Flux: FunctionaL Updates for XML (extended report) (2008)
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...
Mechanizing the Metatheory of LF (2008)
Urban, Christian, Cheney, James, Berghofer, Stefan
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...
Stijn Vansummeren, James Cheney
Knowing the origin of data (i.e., where the data was copied or created from)—its provenance—is vital for assessing the trustworthiness of contemporary scientific databases such as UniProt [16]...
Q2 SELECT Name, ’200 ’ AS Height FROM People WHERE Name = ’James’ (2008)
Provenance is information that aids understanding and troubleshooting database queries by explaining the results in terms of the input. Slicing is a program analysis technique for debugging and...
Principles of Provenance Theme Proposal (2008)
Peter Buneman, James Cheney, Bertram Ludaescher
Theme topic and brief description Recent research in a variety of settings (databases and data warehouses [10, 7, 20, 8], file systems [17], geographic information systems [6], scientific workflows...
Preserving Scientific Data with XMLArch ∗ (2008)
Peter Buneman, James Cheney, Carwyn Edwards, Irini Fundulaki
Scientific databases are continuously updated either by adding new data or by deleting and/or modifying existing data. It is fairly obvious that it is crucial to preserve historic versions of these...
Stijn Vansummeren, James Cheney
Knowing the origin of data (i.e., where the data was copied or created from)—its provenance—is vital for assessing the trustworthiness of contemporary scientific databases such as UniProt [16]...
Regular Expression Subtyping for XML Query and Update Languages (2008)
Abstract. XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be equivalent: a...
Simple nominal type theory (2008)
Abstract. Nominal logic is an extension of first-order logic with features useful for reasoning about abstract syntax with bound names. For computational applications such as programming and formal...
Q2 SELECT Name, ’200 ’ AS Height FROM People WHERE Name = ’James’ (2008)
Provenance is information that aids understanding and troubleshooting database queries by explaining the results in terms of the input. Slicing is a program analysis technique for debugging and...
Abstract A Lightweight Implementation of Generics and Dynamics (2008)
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...
Scrap your Nameplate - Functional Pearl (2008)
Recent research has shown how boilerplate code, or repetitive code for traversing datatypes, can be eliminated using generic programming techniques already available within some implementations of...
Provenance in Manually Curated Databases (2008)
Peter Buneman, Adriane Chapman, James Cheney, Stijn Vansummeren
Many curated databases are constructed by scientists integrating various existing data sources. Most current approaches to provenance in databases are based on views and fail to take account of the...
Regular Expression Subtyping for XML Query and Update Languages (2008)
XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be equivalent: a declarative...
On the Expressiveness of Implicit Provenance in Query and Update Languages (2008)
BUNEMAN, Peter, CHENEY, James, VANSUMMEREN, Stijn
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...
BUNEMAN, Peter, CHENEY, James, TAN, Wang-Chiew, VANSUMMEREN, Stijn
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 --...
Learning Programming Language Parsing Rules (2007)
Modern programming languages have some natural language properties, such as scoping/precedence ambiguities regarding arithmetic operators (e. g. + vs. *) and word (symbol) sense ambiguities (e. g....
Abstract. Prolog is a prototype logic programming language with a built-in notion of binders and unication modulo -equivalence. It is based on a mild extension of rst-order Horn formulae: instead of...
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
Cyclone is a safe dialect of C. It has been designed from the ground up to prevent the buer over ows, format string attacks, and memory management errors that are common in C programs, while...
Abstract A Lightweight Implementation of Generics and Dynamics (2007)
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...
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
Cyclone is a safe dialect of C. It has been designed from the ground up to prevent the buer over ows, format string attacks, and memory management errors that are common in C programs, while...
Theorem Prover Usability (2007)
There is a large research group in the Cornell CS department on automated reasoning and theorem proving. They have developed a system of formal mathematics and a program called Nuprl[5] that allows...
Quantum mechanics is the best known explanation for microscopic physical phenomena. It was developed over the rst half of the twentieth century to account for behaviors such as the discrete energy...
Shape Analysis and Cache Locality for Recursive Data Structures in Java (2007)
There is already a substantial amount of practical research into optimizing programs with static, sequential, array-based data structures. Numerical programs in particular tend to make heavy use of...
Provenance as Dependency Analysis (2007)
Cheney, James, Ahmed, Amal, Acar, Umut
Provenance is information recording the source, derivation, or history of some information. Provenance tracking has been studied in a variety of settings; however, although many design points have...
Repairing Inconsistent XML Write-Access Control Policies (2007)
Bravo, Loreto, Cheney, James, Fundulaki, Irini
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....
Recording Provenance for SQL Queries and Updates (2007)
VANSUMMEREN, Stijn, CHENEY, James
Knowing the origin of data (i.e., where the data was copied or created from)---its provenance---is vital for assessing the trustworthiness of contemporary scientific databases such as UniProt and...
On the Expressiveness of Implicit Provenance in Query and Update Languages (2007)
BUNEMAN, Peter, CHENEY, James, VANSUMMEREN, Stijn
Information concerning the origin of data (that is, its provenance) is important in many areas, especially scientific recordkeeping. Currently, provenance information must be maintained explicitly,...
Recording Provenance for SQL Queries and Updates (2007)
VANSUMMEREN, Stijn, CHENEY, James
Knowing the origin of data (i.e., where the data was copied or created from)---its provenance---is vital for assessing the trustworthiness of contemporary scientific databases such as UniProt and...
On the Expressiveness of Implicit Provenance in Query and Update Languages (2007)
BUNEMAN, Peter, CHENEY, James, VANSUMMEREN, Stijn
Information concerning the origin of data (that is, its provenance) is important in many areas, especially scientific recordkeeping. Currently, provenance information must be maintained explicitly,...
Mechanized metatheory model-checking (2007)
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable...
Provenance as dependency analysis (2007)
James Cheney, Amal Ahmed, Umut A. Acar
Abstract. Provenance is information recording the source, derivation, or history of some information. Provenance tracking has been studied in a variety of settings; however, although many design...
Mechanized metatheory model-checking (2007)
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable...
On the expressiveness of implicit provenance in query and update languages (2007)
Peter Buneman, James Cheney, Stijn Vansummeren
Abstract. Information concerning the origin of data (that is, its provenance) is important in many areas, especially scientific recordkeeping. Currently, provenance information must be maintained...
Provenance as dependency analysis (2007)
James Cheney, Amal Ahmed, Umut A. Acar
Abstract. Provenance is information recording the source, derivation, or history of some information. Provenance tracking has been studied in a variety of settings; however, although many design...
Nominal Logic Programming (2006)
Cheney, James, Urban, Christian
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,...
Completeness and Herbrand theorems for nominal logic (2006)
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 and freshness. It relies on two important...
Completeness and Herbrand Theorems for Nominal Logic (2006)
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 and freshness. It relies on two important...
Tradeoffs in XML Database Compression (2006)
Large XML data files, or XML databases, are now a common way to distribute scientific and bibliographic data, and storing such data e#ciently is an important concern. A number of approaches to XML...
Provenance Management in Curated Databases (2006)
Peter Buneman, Adriane P. Chapman, James Cheney
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...
Logic Column 14: Nominal Logic and Abstract Syntax (2005)
Formalizing syntactic proofs of properties of logics, programming languages, security protocols, and other formal systems is a significant challenge, in large part because of the obligation to handle...
A Simpler Proof Theory for Nominal Logic (2005)
Nominal logic is a variant of first-order logic which provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over...
An Empirical Evaluation of Simple DTD-Conscious Compression Techniques (2005)
this paper, the term "XML compression " is used in the first (and, we believe, original and most accurate) sense exclusively. We will compare our proposed techniques only with other...
A Simpler Proof Theory for Nominal Logic (2005)
Nominal logic is a variant of first-order logic equipped with a "freshname quantifier" N and other features useful for reasoning about languages with bound names. Its original presentation...
Relating Nominal and Higher-Order Pattern Unification (2005)
Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of #-equivalence (consistent renaming of bound names). Though the higher-order and nominal...
A Copy-and-Paste Model for Provenance in Curated Databases (2005)
Provenance is information describing the origin, construction, location, ownership, or other aspects of the history of an object. Previous work on provenance has concentrated on an understanding of...
Relating nominal and higher-order pattern unification (2005)
Abstract. Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of α-equivalence (consistent renaming of bound names). The higher-order and nominal...
James Cheney, Livingstone Place (f
United States citizen Research Fellow, University of Edinburgh. Postdoctoral researcher in database group.
A Sequent Calculus for Nominal Logic (2004)
Murdoch Gabbay, James Cheney, Lix École Polytechnique
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...
Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence (2004)
There are two well-known approaches to programming with names, binding, and equivalence up to consistent renaming: representing names and bindings as concrete identifiers in a first-order language...
Equivariant Unification (2004)
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of...
Avoiding Equivariance in Alpha-Prolog (2004)
Prolog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed #-calculi and many other languages involving bound names. In...
The Semantics of Nominal Logic Programs (2004)
Nominal logic programming is a form of logic programming with "concrete" names and binding, based on nominal logic, a theory of alpha-equivalence founded on swapping and freshness...
First-Class Phantom Types (2003)
Classical phantom types are datatypes in which type constraints are expressed using type variables that do not appear in the datatype cases themselves. They can be used to embed typed languages into...
First-Class Phantom Types (2003)
Classical phantom types are datatypes in which type constraints are expressed using type variables that do not appear in the datatype cases themselves. They can be used to embed typed languages into...
A Linearly Typed Assembly Language (2003)
Cheney, James, Morrisett, Greg
Today's type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that ``stands on its own'': it...
A Linearly Typed Assembly Language (2003)
Cheney, James, Morrisett, Greg
Today's type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that ``stands on its own'': it...
Phantom types are data types with type constraints associated with dierent cases. Examples of phantom types include typed type representations and typed higher-order abstract syntax trees. These...
First-class phantom types (2003)
Abstract. Phantom types are data types with type constraints associated with different cases. Examples of phantom types include typed type representations and typed higher-order abstract syntax...
Region-based memory management in Cyclone (2002)
Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, James Cheney
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....
Region-based memory management in Cyclone (2002)
Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, James Cheney
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....
XParse: A Language for Parsing Text to XML (2002)
This paper presents a domain-specific language, XParse, that attempts to combine the power of tools like lex and yacc, which generate efficient parsers from declarative specifications, with the...
Cyclone: A safe dialect of C (2002)
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
Cyclone is a safe dialect of C. It has been designed from the ground up to prevent the bu#er overflows, format string attacks, and memory management errors that are common in C programs, while...
A Lightweight Implementation of Generics and Dynamics (2002)
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...
Formal Type Soundness for Cyclone's Region System (2001)
Grossman, Dan, Jim, Trevor, Hicks, Mike, Wang, Yanling, Cheney, James
Cyclone is a polymorphic, type-safe programming language derived from C\@. The primary design goals of Cyclone are to let programmers control data representations and memory management without...
Formal Type Soundness for Cyclone's Region System (2001)
Grossman, Dan, Jim, Trevor, Hicks, Mike, Wang, Yanling, Cheney, James
Cyclone is a polymorphic, type-safe programming language derived from C\@. The primary design goals of Cyclone are to let programmers control data representations and memory management without...
Cyclone User's Manual, Version 0.1.3 (2001)
Grossman, Dan, Jim, Trevor, Hicks, Michael, Wang, Yanling, Cheney, James
The current version of this manual should be available at http://www.cs.cornell.edu/projects/cyclone/ and http://www.research.att.com/projects/cyclone/. The version here describes Cyclone Version...
Cyclone User's Manual, Version 0.1.3 (2001)
Grossman, Dan, Jim, Trevor, Hicks, Michael, Wang, Yanling, Cheney, James
The current version of this manual should be available at http://www.cs.cornell.edu/projects/cyclone/ and http://www.research.att.com/projects/cyclone/. The version here describes Cyclone Version...
Toward a Theory of Information Preservation (2001)
Cheney, James, Lagoze, Carl, Botticelli, Peter
Digital preservation is a pressing challenge to the library community. In this paper, we describe the initial results of our efforts towards understanding digital (as well as traditional)...
Toward a Theory of Information Preservation (2001)
Cheney, James, Lagoze, Carl, Botticelli, Peter
Digital preservation is a pressing challenge to the library community. In this paper, we describe the initial results of our efforts towards understanding digital (as well as traditional)...
Formal type soundness for Cyclone’s region system (2001)
Dan Grossman, Greg Morrisett, Trevor Jim, Mike Hicks, Yanling Wang, James Cheney
Formal type soundness for Cyclone’s region system (2001)
Dan Grossman, Greg Morrisett, Trevor Jim, Mike Hicks, Yanling Wang, James Cheney
Cyclone is a polymorphic, type-safe programming language derived from C. The primary design goals of Cyclone are to let programmers control data representations and memory management without...
Compressing XML with multiplexed hierarchical PPM models (2001)
Extensible Markup Language (XML) is a standardized language that \describes a class of data objects called XML documents and partially describes the behavior of computer programs which process...
Formal type soundness for Cyclone’s region system (2001)
Dan Grossman, Greg Morrisett, Trevor Jim, Mike Hicks, Yanling Wang, James Cheney
Cyclone is a polymorphic, type-safe programming language derived from C. The primary design goals of Cyclone are to let programmers control data representations and memory management without...
Statistical models for term compression (2000)
Symbolic tree data structures, or terms, are used in many computing systems. Although terms can be compressed by hand, using specialized algorithms, or using universal compression utilities, all of...
Reasoning Constructively about Probability and Programming with Chance (1999)
this report I will describe some of the main approaches taken by mathematicians, logicians, and computer scientists in formalizing uncertainty. I will outline the advantages and disadvantages of...
Stack-based Typed Assembly Language (1998)
Today's type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that \stands on its...
Stack-based Typed Assembly Language (1998)
Today’s type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that “stands on its own”: it...
The Complexity of Equivariant Unification
Nominal logic is a first-order theory of names and binding based on a primitive operation of swapping rather than substitution. Urban, Pitts, and Gabbay have developed a nominal unification algorithm...