Related papers: A New Perspective for Hoare's Logic and Peano's Ar…
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In…
The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic --- see http://www.cis.upenn.edu/~giorgi/cl.html): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete…
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed, using an abstract…
This paper focuses on the expressive power of disjunctive and normal logic programs under the stable model semantics over finite, infinite, or arbitrary structures. A translation from disjunctive logic programs into normal logic programs is…
A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these…
Classical logic predicts that everything (thus nothing useful at all) follows from inconsistency. A paraconsistent logic is a logic where an inconsistency does not lead to such an explosion, and since in practice consistency is difficult to…
In this paper, we introduce a foundation for computable model theory of rational Pavelka logic (an extension of {\L}ukasiewicz logic) and continuous logic, and prove effective versions of some theorems in model theory. We show how to reduce…
Vardanyan's Theorems state that $\mathsf{QPL}(\mathsf{PA})$ - the quantified provability logic of Peano Arithmetic - is $\Pi^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary…
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected…
This paper presents an extension to Hoare logic for pointer program verification. Logic formulas with user-defined recursive functions are used to specify properties on the program states before/after program executions. Three basic…
A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted…
We describe a mathematical structure that can give extensional denotational semantics to higher-order probabilistic programs. It is not limited to discrete probabilities, and it is compatible with integration in a way the models that have…
We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different…
We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories…
Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties…
The overarching theme of the following pages is that mathematical logic -- centered around the incompleteness theorems -- is first and foremost an investigation of $\textit{computation}$, not arithmetic. Guided by this intuition we will…
Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive…
We augment LP with a strong conditional operator, to yield a logic we call "strong LP," or LP=>. The resulting logic can speak of consistency in more discriminating ways, but introduces new possibilities for trivializing paradoxes.
We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique…
We show that it is provable in PA that there is an arithmetically definable sequence $\{\phi_{n}:n \in \omega\}$ of $\Pi^{0}_{2}$-sentences, such that - PRA+$\{\phi_{n}:n \in \omega\}$ is $\Pi^{0}_{2}$-sound and $\Pi^{0}_{1}$-complete - the…