Home

Publications

Presentations

Programs

BibTeX entries for all publications

Hot off the press

• The Rationale of PROV, Luc Moreau, Paul Groth, James Cheney, Simon Miles and Timothy Lebo, Journal of Web Semantics, to appear.
• Notions of bidirectional computation and entangled state monads, Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna and Perdita Stevens, MPC 2015, to appear.
• A simple sequent calculus for nominal logic, James Cheney. Journal of Logic and Computation, special issue in honor of Roy Dyckhoff. Published online, May 2014.

Journal Articles

• The Rationale of PROV, Luc Moreau, Paul Groth, James Cheney, Simon Miles and Timothy Lebo, Journal of Web Semantics, to appear.
• A simpler proof theory for nominal logic, James Cheney. To appear, Journal of Logic and Computation, special issue in honor of Roy Dyckhoff.
• A core calculus for provenance, Umut A. Acar, Amal Ahmed, James Cheney and Roly Perera. Journal of Computer Security 21(6):919-969, 2013 (Special Issue on POST 2012)
• Revisiting "Forward Node-Selecting Queries over Trees", James Cheney. Transactions on Database Systems 38(2):13, 2013. (Preprint)
• Consistency and Repair for XML Write-Access Policies, Loreto Bravo, James Cheney, Irini Fundulaki, and Ricardo Segovia. VLDB Journal 21(6):843-867, 2012.
• Requirements for Provenance on the Web, Paul Groth, Yolanda Gil, James Cheney and Simon Miles, International Journal of Digital Curation 8(1):39-56, 2012.
• A dependent nominal type theory, LMCS volume 8(1:8), 2012 (special issue for TYPES 2010). (arXiv)
• Provenance as Dependency Analysis. James Cheney, Amal Ahmed and Umut Acar. Mathematical Structures in Computer Science 21(6): 1301-1337 (2011).
• Formalizing adequacy for higher-order abstract syntax. James Cheney, Rene Vestergaard and Michael Norrish. Journal of Automated Reasoning 49(2):209--239, 2012. Special issue on TAASN 2009 (revised September 2010, published online February 2011). Formal development here.
• Mechanizing the metatheory of LF. Christian Urban, James Cheney, and Stefan Berghofer. Transactions on Computational Logic. 12(2):A15, January 2011. Formal development here.
• Equivariant unification. James Cheney. Journal of Automated Reasoning 45(3):267-300, 2010.
• On the expressiveness of implicit provenance in query and update languages, P. Buneman, J. Cheney and S. Vansummeren. Transactions on Database Systems, 33(4):28 November 2008.
• Nominal Logic Programming, J. Cheney and C. Urban. Transactions on Programming Languages and Systems, 30(5):26 August 2008.
• Completeness and Herbrand theorems for nominal logic, James Cheney, Journal of Symbolic Logic, 71(1), 299-320, 2006.
• An X-ray diffraction simulator for undergraduate crystallography, J. Cheney and M. de Graef, Journal of Materials Education, 18:57-66, 1996

Refereed Conference Papers

• Notions of bidirectional computation and entangled state monads, Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna and Perdita Stevens, MPC 2015, to appear.
• Dynamic provenance for SPARQL Updates, Harry Halpin and James Cheney, ISWC 2014, p. 425-440 (arxiv)
• Database Queries that Explain their Work, James Cheney, Amal Ahmed and Umut Acar. PPDP 2014, p. 271-282 (arXiv)
• Query shredding: Efficient relational evaluation of queries over nested multisets, Sam Lindley, James Cheney and Philip Wadler. SIGMOD 2014, p. 1027-1038. (arxiv, code)
• Effective Quotation, James Cheney, Sam Lindley, Gabriel Radanne, and Philip Wadler. PEPM 2014. (arxiv, code)
• A practical theory of language-integrated query, James Cheney, Sam Lindley and Phil Wadler. ICFP 2013, p. 403-416. See also supplementary material available here.
• Functional Programs that Explain their Work, Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. ICFP 2012, p. 365-376.
• A core calculus for provenance, Umut A. Acar, Amal Ahmed, James Cheney and Roly Perera. POST 2012.
• Mechanizing the Metatheory of mini-XQuery, James Cheney and Christian Urban. CPP 2011. Formalization here.
• A formal framework for provenance security, James Cheney. CSF 2011.
• Satisfiability algorithms for conjunctive queries over trees, James Cheney. ICDT 2011, p. 150-161.
• Destabilizers and independence of XML updates, Michael Benedikt and James Cheney. VLDB 2010, p. 906-917.
• Provenance: A Future History, James Cheney, Steve Chong, Nate Foster, Margo Seltzer, Stijn Vansummeren. Onward! 2009.
• Schema-Based Independence Analysis for XML Updates, Michael Benedikt and James Cheney. VLDB 2009, p. 61-72. (technical report)
• Semantics, Types and Effects for XML Updates, Michael Benedikt and James Cheney. DBPL 2009, p. 1-17. (technical report)
• Estimating the Distribution and Propagation of Genetic Programming Building Blocks through Tree Compression. Bob McKay, Xuan Hoai Nguyen, James Cheney, Min Hyeok Kim and Naoki Mori. GECCO 2009, p. 1011-1018.
• FLUX: FunctionaL Updates for XML. James Cheney. ICFP 2008, p. 3-14. (arXiv)
• Mechanizing the metatheory of LF. Christian Urban, James Cheney, and Stefan Berghofer. LICS 2008, p. 45-56. Superseded by TOCL article. (arXiv)
• Regular Expression Subtyping for XML Query and Update Languages, James Cheney, ESOP 2008, p. 32-46. (arXiv)
• Provenance as Dependency Analysis. James Cheney, Amal Ahmed and Umut Acar. DBPL 2007, p. 139-153. (arXiv) Superseded by MSCS article.
• Repairing Inconsistent XML Write-Access Control Policies. Loreto Bravo, James Cheney and Irini Fundulaki, DBPL 2007, p. 98-112. Superseded by VLDBJ article. (arXiv)
• Mechanized Metatheory Model-Checking, James Cheney and Alberto Momigliano, PPDP 2007, p. 75-86.
• On the Expressiveness of Implicit Provenance in Query and Update Languages, Peter Buneman, James Cheney, and Stijn Vansummeren. ICDT 2007, Volume 4353 of Lecture Notes in Computer Science, p. 209-223. (Springer)
• The Semantics of Nominal Logic Programs, James Cheney. ICLP 2006, p. 361 - 375. (Errata) (Springer)
• Provenance Management in Curated Databases. Peter Buneman, Adriane Chapman, and James Cheney. SIGMOD 2006, p. 539 - 550.
• Tradeoffs in XML Database Compression, James Cheney, DCC 2006, p. 392-491. (IEEE)
• Scrap your Nameplate (Functional Pearl), ICFP 2005. pp 180-191.
• Avoiding Equivariance in Alpha-Prolog, Christian Urban and James Cheney. TLCA 2005, pp. 401-416. (Springer)
• Equivariant Unification, James Cheney. RTA 2005, pp. 74-89. (Springer)
• A Simpler Proof Theory for Nominal Logic, James Cheney. FOSSACS 2005, pp. 379-394. (Springer)
• AlphaProlog: A Logic Programming Language with Names, Binding and alpha-equivalence, James Cheney and Christian Urban. ICLP 2004, p. 269-283. (Springer)
• A Sequent Calculus for Nominal Logic, Murdoch Gabbay and James Cheney. LICS 2004, p. 139-148. (IEEE)
• The Complexity of Equivariant Unification, James Cheney. ICALP 2004, p. 332-344. (Springer)
• A lightweight implementation of generics and dynamics, James Cheney and Ralf Hinze. Haskell Workshop 2002, Pittsburgh, PA, 2002.
• Cyclone: A Safe Dialect of C, Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang. USENIX Annual Technical Conference, p. 275-288, Monterey, CA, June 2002.
• Region-based Memory Management in Cyclone, Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. ACM Conference on Programming Language Design and Implementation, pages 282-293, Berlin, Germany, June, 2002.
• Toward a Theory of Information Preservation (Abbreviated Conference Version), James Cheney, Carl Lagoze and Peter Botticelli, 5th European Conference on Research and Advanced Technology for Digital Libraries (ECDL 2001), Darmstadt, 2001.
• Compressing XML with Multiplexed Hierarchical Models, James Cheney, in Proceedings of the 2001 IEEE Data Compression Conference, pp. 163-172.

Proceedings

• Principles of Provenance (Dagstuhl Seminar 12091), James Cheney and Anthony Finkelstein and Bertram Ludaescher and Stijn Vansummeren, Dagstuhl Reports, 2(2):84-113.
• Proceedings of the First Workshop on Cross-Model Language Design and Implementation, James Cheney and Torsten Grust. Informal proceedings.
• Proceedings of the First Workshop on the Theory and Practice of Provenance, James Cheney, editor, February 23, 2009, San Francisco, CA, USA.
• LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, James Cheney and Amy Felty, editors, August 2, 2009, Montreal, Quebec, Canada.

Invited papers

• Toward a theory of self-explaining computation, James Cheney, Umut A. Acar and Roly Perera. Festschrift for Peter Buneman, p. 193-216, LNCS 8000.
• The Database Wiki project, Peter Buneman, James Cheney, Sam Lindley and Heiko Mueller, SIGMOD Record Systems & Prototypes column.
• Is provenance logical?, James Cheney, invited talk, LID 2011.
• Provenance in databases: Why, where and how, J. Cheney, L. Chiticariu and W.-C. Tan. Foundations and Trends in Databases, 1(4):379-474, 2009.
• Provenance, XML and the Scientific Web. James Cheney, PLAN-X 2009.
• Curated Databases, Peter Buneman, James Cheney, Wang-Chiew Tan and Stijn Vansummeren. PODS 2008, p. 1-12.
• Recording Provenance for SQL Queries and Updates, Stijn Vansummeren and James Cheney. IEEE Data Engineering Bulletin, 30(4):29-37, December 2007.
• Program slicing and data provenance, James Cheney. IEEE Data Engineering Bulletin, 30(4):22-28, December 2007.

Workshop Papers

• An analytical survey of provenance sanitization, James Cheney and Roly Perera, IPAW 2014. (arxiv)
• Toward a repository of BX examples, James Cheney and James McKinna and Perdita Stevens and Jeremy Gibbons, postproceedings of BX 2014, CEUR-WS volume 1133:87--91, 2014.
• Entangled State Monads, James Cheney and James McKinna and Perdita Stevens and Jeremy Gibbons and Faris Abou-Saleh, postproceedings of BX 2014, CEUR-WS volume 1133:108-111, 2014.
• Lenses for Web Data, postproceedings of BX 2013, EC-EASST volume 57. Raghu Rajkumar, Sam Lindley, Nate Foster, James Cheney.
• Semantics and Provenance for Processing Element Composition in Dispel Workflows, Eric Griffis, Paul Martin and James Cheney, WORKS 2013.
• Static Enforceability of XPath-Based Access Control Policies, DBPL 2013.
• Provenance for seismological processing pipelines in a distributed streaming workflow Alessandro Spinuso, James Cheney, Malcolm Atkinson, BigProv 2013
• Toward provenance-based security for configuration languages. Paul Anderson and James Cheney. TAPP 2012.
• Hierarchical models of provenance. Peter Buneman, James Cheney, and Egor Kostylev. TAPP 2012.
• Row-based effect types for database integration, Sam Lindley and James Cheney, TLDI 2012.
• Using Links to prototype a Database Wiki, James Cheney, Sam Lindley and Heiko Mueller, DBPL 2011.
• Higher-order unification for the lambda-alpha-nu calculus, Ben Kavanagh and James Cheney, UNIF 2011.
• Dynamic provenance for SPARQL Updates using Named Graphs. Harry Halpin and James Cheney. TAPP 2011.
• Causality and the semantics of provenance, James Cheney. DCM 2010.
• A graph model of data and workflow provenance, Umut Acar, Peter Buneman, James Cheney, Jan Van den Bussche, Natalia Kwasnikowska, and Stijn Vansummeren. TAPP 2010.
• Formalizing adequacy. James Cheney, Rene Vestergaard and Michael Norrish. TAASN 2009.
• Simple Nominal Type Theory. James Cheney. LFMTP 2008. An initial formalization of key syntactic properties is here.
• Resource Bound Analysis for Database Queries. James Cheney and Morten Dahl. PLAS 2008.
• Lux: A lightweight, statically-typed language for updating XML, PLAN-X 2007 (informal proceedings)
• A Provenance Model for Manually Curated Data, Peter Buneman, Adriane Chapman, James Cheney, and Stijn Vansummeren. 2006 International Provenance and Annotation Workshop (IPAW 2006), LNCS 4145, 162-170. (Springer)
• Towards a General Theory of Names, Binding and Scope, MERLIN 2005. pp 33-40.
• An Empirical Evaluation of Simple DTD-Conscious Compression Techniques, WebDB 2005. (ps)
• Relating Higher-Order Pattern Unification and Nominal Unification, James Cheney. Proceedings of UNIF 2005, p. 104-119
• System Description: alpha-Prolog, a Fresh Approach to Logic Programming Modulo alpha-Equivalence, James Cheney and Christian Urban. UNIF 2003, Valencia, Spain, 2003.

Tutorials

• The W3C PROV family of specifications for modelling provenance metadata, Paolo Missier, Khalid Belhajjame, and James Cheney. EDBT 2013 tutorial.

Columns

• Event Report: Workshop on Theory and Practice of Provenance. James Cheney. SIGMOD Record 38(2):57-60, 2009.
• Report on the Principles of Provenance Workshop. James Cheney, Peter Buneman and Bertram Ludaescher. SIGMOD Record 37(1):62-65, 2008.
• Nominal Logic and Abstract Syntax, Logic Column, SIGACT News 36(4), p. 47-69, December 2005. (arxiv)

  In this paper, I identified some properties of higher-order abstract syntax techniques, primarily as employed in LF, where I think some improvement may be possible. Karl Crary and Robert Harper of CMU responded to these criticisms in a subsequent logic column.

Posters and Demos

• DBWiki: A Structured Wiki for Curated Data and Collaborative Data Management , Peter Buneman, James Cheney, Sam Lindley and Heiko Mueller. Demo, SIGMOD 2011.
• ACCOn: Checking Consistency of XML Write-Access Control Policies, Loreto Bravo, James Cheney and Irini Fundulaki. Demo, EDBT 2008.
• Statistical Modeling for Term Compression, James Cheney, in Proceedings of the 2000 IEEE Data Compression Conference, p. 550. (full version)

Technical Reports

• Provenance Traces, James Cheney, Umut A. Acar and Amal Ahmed.
• A Simpler Proof Theory for Nominal Logic, James Cheney. Technical Report EDI-INF-RR-0237, School of Informatics, University of Edinburgh.
• A Linearly Typed Assembly Language. James Cheney and Greg Morrisett. CUCIS TR2003-1900.
• First-Class Phantom Types. James Cheney and Ralf Hinze. CUCIS TR2003-1901. (errata)
• Formal Type Soundness for Cyclone's Region System, Dan Grossman, Greg Morrisett, Trevor Jim, Mike Hicks, Yanling Wang and James Cheney. CUCS TR2001-1856.
• Cyclone User's Manual, Version 0.1.3, Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang and James Cheney. CUCS TR2001-1855.
• Toward a Theory of Information Preservation (Complete Version), James Cheney, Carl Lagoze and Peter Botticelli. Cornell University, Ithaca, Computer Science Technical Report TR2001-1841.

Dissertations and Theses

• Nominal Logic Programming, James Cheney, PhD dissertation, Cornell University, August 2004. (PDF)
• First-order Term Compression: Techniques and Applications, James Cheney, Master's thesis, Carnegie Mellon University, August 1998.