Volume 11, Issue 1

2015


1. A Hoare logic for the coinductive trace-based big-step semantics of While

Nakata, Keiko ; Uustalu, Tarmo.
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for While. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) […]

2. Permission-Based Separation Logic for Multithreaded Java Programs

Haack, Christian ; Huisman, Marieke ; Hurlin, Clément ; Amighi, Afshin.
This paper presents a program logic for reasoning about multithreaded Java-like programs with dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptation of concurrent separation logic to a […]

3. Monads need not be endofunctors

Altenkirch, Thosten ; Chapman, James ; Uustalu, Tarmo.
We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore […]

4. On the relative proof complexity of deep inference via atomic flows

Das, Anupam.
We consider the proof complexity of the minimal complete fragment, KS, of standard deep inference systems for propositional logic. To examine the size of proofs we employ atomic flows, diagrams that trace structural changes through a proof but ignore logical information. As results we obtain a […]

5. Program Logics for Homogeneous Generative Run-Time Meta-Programming

Berger, Martin ; Tratt, Laurence.
This paper provides the first program logic for homogeneous generative run-time meta-programming---using a variant of MiniML by Davies and Pfenning as its underlying meta-programming language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We […]

6. Extracting verified decision procedures: DPLL and Resolution

Berger, Ulrich ; Lawrence, Andrew ; Forsberg, Fredrik Nordvall ; Seisenberger, Monika.
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and […]

7. Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq

Schmidt-Schauß, Manfred ; Sabel, David ; Machkasova, Elena.
This paper shows equivalence of several versions of applicative similarity and contextual approximation, and hence also of applicative bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and […]

8. The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems

Normann, Dag.
We investigate wether three statements in analysis, that can be proved classically, are realizable in the realizability model of extensional continuous functionals induced by Kleene's second model $K_2$. We prove that a formulation of the Riemann Permutation Theorem as well as the statement that all […]

9. Complexity of Problems of Commutative Grammars

Kopczynski, Eryk.
We consider commutative regular and context-free grammars, or, in other words, Parikh images of regular and context-free languages. By using linear algebra and a branching analog of the classic Euler theorem, we show that, under an assumption that the terminal alphabet is fixed, the membership […]

10. Weak Cat-Operads

DOSEN, Kosta ; Petric, Zoran.
An operad (this paper deals with non-symmetric operads)may be conceived as a partial algebra with a family of insertion operations, Gerstenhaber's circle-i products, which satisfy two kinds of associativity, one of them involving commutativity. A Cat-operad is an operad enriched over the category […]

11. Effective zero-dimensionality for computable metric spaces

Kenny, Robert.
We begin to study classical dimension theory from the computable analysis (TTE) point of view. For computable metric spaces, several effectivisations of zero-dimensionality are shown to be equivalent. The part of this characterisation that concerns covering dimension extends to higher dimensions and […]

12. The Computational Complexity of Propositional Cirquent Calculus

Bauer, Matthew Steven.
Introduced in 2006 by Japaridze, cirquent calculus is a refinement of sequent calculus. The advent of cirquent calculus arose from the need for a deductive system with a more explicit ability to reason about resources. Unlike the more traditional proof-theoretic approaches that manipulate tree-like […]

13. Positive Inductive-Recursive Definitions

Ghani, Neil ; Forsberg, Fredrik Nordvall ; Malatesta, Lorenzo.
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive […]

14. Bialgebraic Semantics for Logic Programming

Bonchi, Filippo ; Zanasi, Fabio.
Bialgebrae provide an abstract framework encompassing the semantics of different kinds of computational models. In this paper we propose a bialgebraic approach to the semantics of logic programming. Our methodology is to study logic programs as reactive systems and exploit abstract techniques […]

15. High-level Counterexamples for Probabilistic Automata

Wimmer, Ralf ; Jansen, Nils ; Ã?brahÃ?m, Erika ; Katoen, Joost-Pieter.
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of […]

16. Ranking Templates for Linear Loops

Leike, Jan ; Heizmann, Matthias.
We present a new method for the constraint-based synthesis of termination arguments for linear loop programs based on linear ranking templates. Linear ranking templates are parameterized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. Our […]

17. Domain Representations Induced by Dyadic Subbases

Tsuiki, Hideki ; Tsukamoyo, Yasuyuki.
We study domain representations induced by dyadic subbases and show that a proper dyadic subbase S of a second-countable regular space X induces an embedding of X in the set of minimal limit elements of a subdomain D of $\{0,1,\perp\}\omega$. In particular, if X is compact, then X is a retract […]

18. Modelling MAC-Layer Communications in Wireless Systems

Cerone, Andrea ; Hennessy, Matthew ; Merro, Massimo.
We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of […]

19. Kernelizing MSO Properties of Trees of Fixed Height, and Some Consequences

Gajarsky, Jakub ; Hlineny, Petr.
Fix an integer h>=1. In the universe of coloured trees of height at most h, we prove that for any graph decision problem defined by an MSO formula with r quantifiers, there exists a set of kernels, each of size bounded by an elementary function of r and the number of colours. This yields two […]

20. Aspect-oriented linearizability proofs

Chakraborty, Soham ; Henzinger, Thomas A. ; Sezgin, Ali ; Vafeiadis, Viktor.
Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking […]