A Equivalence of the Original and Refined Semantics In this appendix, we wish show that the refined semantics given in Section 6.2 is equivalent to the semantics given in Section 4, in the sense that...
Under consideration for publication in J. Functional Programming 1 Transactional Events∗ (2008)
Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional...
Soundness of the Formal Model for Active Adversaries (2008)
Much of the content of these notes (in particular most of the definitions) is taken verbatim from [3]. 1
Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional...
SYSTEM F WITH CONSTRAINT TYPES (2008)
Kevin Donnelly, Hongwei Xi Phd, Assaf Kfoury Phd, Kevin Donnelly
System F is a type system that can be seen as both a proof system for second-order propositional logic and as a polymorphic programming language. In this work we explore several extensions of System...
On the Stable Paths Problem and a Restricted Variant (2008)
Interdomain routing on the Internet is performed using route preference policies specified independently, and arbitrarily by each Autonomous System in the network. These policies are used in the...
A decision procedure for linear "big O" equations (2007)
Avigad, Jeremy, Donnelly, Kevin
Let $F$ be the set of functions from an infinite set, $S$, to an ordered ring, $R$. For $f$, $g$, and $h$ in $F$, the assertion $f = g + O(h)$ means that for some constant $C$, $|f(x) - g(x)| \leq C...
System F with type equality coercions (2007)
Martin Sulzmann, Simon Peyton Jones, Kevin Donnelly
We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric...
Urban rhetorics and rhetorics of urbanity : eighteenth-century criollo writings of the city / (2006)
Typescript.
We formalize in the logical framework ATS/LF a proof based on Tait’s method that establishes the simply-typed lambda-calculus being strongly normalizing. In this formalization, we employ...
A formally verified proof of the prime number theorem (2006)
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1 / ln x. Whereas their...
A formally verified proof of the prime number theorem (2005)
Avigad, Jeremy, Donnelly, Kevin, Gray, David, Raff, Paul
The prime number theorem, established by Hadamard and de la Vall'ee Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1 / ln x. Whereas their...
The spectre of sound: music in film and television (2005)
This book is a major new study - dealing with notions of film music as a device that desires to control its audience, using a most powerful thing: emotion. The author emphasises the manipulative and...
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
A formally verified proof of the
Combining higher-order abstract syntax with first-order abstract syntax in ATS (2005)
Abstract Encodings based on higher-order abstract syntax represent the vari-ables of an object-language as the variables of a meta-language. Such encodings allow for the reuse of ff-conversion,...
Ats: A language that combines programming with theorem proving (2005)
Sa Cui, Kevin Donnelly, Hongwei Xi
Abstract. ATS is a language with a highly expressive type system that supports a restricted form of dependent types in which programs are not allowed to appear in type expressions. The language is...
Some Considerations on a Calculus with Weak References (2005)
Kevin Donnelly Boston, Kevin Donnelly, Assaf J. Kfoury
Weak references are references that do not prevent the object they point to from being garbage collected. Most realistic languages, including Java, SML/NJ, and OCaml to name a few, have some facility...
Some Considerations on a Calculus with Weak References (2005)
Kevin Donnelly, Assaf J. Kfoury
Abstract Weak references are references that do not prevent the object they point to from being garbage collected. Most realistic languages, including Java, SML/NJ, and OCaml to name a few, have some...
Kevin Donnelly, Assaf J. Kfoury
Weak references are references that do not prevent the object they point to from being garbage collected. Most realistic languages, including Java, SML/NJ, and OCaml to name a few, have some facility...
Ats: A language that combines programming with theorem proving (2005)
Sa Cui, Kevin Donnelly, Hongwei Xi
Abstract. ATS is a language with a highly expressive type system that supports a restricted form of dependent types in which programs are not allowed to appear in type expressions. The language is...
Formal Semantics of Weak References (2005)
Kevin Donnelly, J. J. Hallett, Assaf Kfoury
Weak references are references that do not prevent the object they point to from being garbage collected. Many realistic languages, including Java, SML/NJ, and Haskell to name a few, support weak...
Some Considerations on a Calculus with Weak References (2005)
Kevin Donnelly, Assaf J. Kfoury
Weak references are references that do not prevent the object they point to from being garbage collected. Most realistic languages, including Java, SML/NJ, and OCaml to name a few, have some facility...
Formalizing O notation in Isabelle/HOL (2004)
Abstract. We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant. 1
Formalizing O notation in Isabelle/HOL (2004)
Abstract. We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant. 1
The Hidden Heritage of Film Music: History and Scholarship (2001)
Contents Introduction Chapter One: The Hidden Heritage of Film Music: History and Scholarship K. J. Donnelly Chapter Two: Analytical and Interpretive Approaches to Film Music (I): Analysing the Music...
Performance and the Composite Film Score (2001)
Contents Introduction Chapter One: The Hidden Heritage of Film Music: History and Scholarship K. J. Donnelly Chapter Two: Analytical and Interpretive Approaches to Film Music (I): Analysing the Music...