Accueil

James Cheney

  1. Causality and the Semantics of Provenance.

    Wed, 06/09/2010 - 15:01 — SomNambul
    Authors: James Cheney
    Subjects: Logic in Computer Science
    Abstract

    Provenance, or information about the sources, derivation, custody or history
    of data, has been studied recently in a number of contexts, including
    databases, scientific workflows and the Semantic Web. Many provenance
    mechanisms have been developed, motivated by informal notions such as
    influence, dependence, explanation and causality. However, there has been
    little study of whether these mechanisms formally satisfy appropriate policies
    or even how to formalize relevant motivating concepts such as causality.

  2. Mechanizing the Metatheory of LF.

    Mon, 10/26/2009 - 14:11 — SomNambul
    Authors: Christian Urban, James Cheney, Stefan Berghofer
    Subjects: Logic in Computer Science
    Abstract

    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.

Math-arch

Syndicate content