A Type-Directed Negation Elimination

if each recursive variable occurs underneath an even number of

negations. By means of De Morgan's laws, it is easy to transform

any well-formed formula in a formula without negations, its negation

normal form.

Moreover, if the initial formula is of size n, its negation normal form is

of size at most n. The full modal mu-calculus and the negation

normal form fragment are thus equally expressive and concise.

In this paper we extend this result to the higher-order fixpoint

logic, an extension of the modal mu-calculus with

higher-order recursive predicate transformers. We present a procedure

that converts a formula of size n into an equivalent formula

without negations of linear size when the number of variables is fixed.

Due to the type system ruling HFL formulas, our procedure significantly

differs from the standard ``negation pushing'' procedure and crucially exploits

type annotations on all subformulas.

Self-Correlation and Maximum Independence in Finite Relations

This paper addresses the problem of finding maximum independent partitions for finite relations, ignoring the order of the attributes. We develop our theory in terms of the finite lattice of partitions of the set of attributes, ordered by refinement, and the lattice of quotient relations it induces. We present a characterisation of independent partitions in terms of the so-called minimal self-correlated sets of attributes (mincors). We consider a transformer on partitions corresponding to merging overlapping mincors combined with relation quotienting. We show that the transformer is not monotone but increasing and show that the maximum independent partition is its least fixed point. We use some additional properties of the transformer to show that this fixed point is still the limit of the standard approximation sequence as in Kleene's well-known fixed point theorem for continuous functions, giving rise to an iterative fixed point computation procedure. The said procedure is efficient, given an oracle for the mincors.

*-Continuous Kleene ω-Algebras for Energy Problems

Disjunctive form and the modal $\mu$ alternation hierarchy

Equivalence of two Fixed-Point Semantics for Definitional Higher-Order Logic Programs

assigning a purely extensional semantics to higher-order

logic programming. The former approach uses classical

domain-theoretic tools while the latter builds on a

fixed-point construction defined on a syntactic instantiation

of the source program. The relationships between these two

approaches had not been investigated until now. In this paper

we demonstrate that for a very broad class of programs,

namely the class of definitional programs introduced

by W. W. Wadge, the two approaches coincide (with respect

to ground atoms that involve symbols of the program).

On the other hand, we argue that if existential higher-order

variables are allowed to appear in the bodies of program rules,

the two approaches are in general different. The results of

the paper contribute to a better understanding of the semantics

of higher-order logic programming.

Formalizing Termination Proofs under Polynomial Quasi-interpretations

Dependent Inductive and Coinductive Types are Fibrational Dialgebras

Iteration Algebras for UnQL Graphs and Completeness for Bisimulation

model graph data in a graph database query language. Around twenty years

ago, Buneman et al. developed a graph database query language UnQL on the top

of a functional meta-language UnCAL for describing and manipulating

graphs. Recently, the functional programming community has shown renewed

interest in UnCAL, because it provides an efficient graph transformation

language which is useful for various applications, such as bidirectional

computation. However, no mathematical semantics of UnQL/UnCAL graphs has

been developed. In this paper, we give an equational axiomatisation and

algebraic semantics of UnCAL graphs. The main result of this paper is to

prove that completeness of our equational axioms for UnCAL for the original

bisimulation of UnCAL graphs via iteration algebras. Another benefit of

algebraic semantics is a clean characterisation of structural recursion on

graphs using free iteration algebra.

Reasoning about modular data-types with Mendler induction

convenient modular representation of recursive datatypes, based on

their initial algebra semantics. Unfortunately it is highly

challenging to implement this technique in proof assistants that are

based on type theory, like Coq. The reason is that it involves type

definitions, such as those of type-level fixpoint operators, that are

not strictly positive. The known work-around of impredicative

encodings is problematic, insofar as it impedes conventional inductive

reasoning. Weak induction principles can be used instead, but they

considerably complicate proofs.

This paper proposes a novel and simpler technique to reason

inductively about impredicative encodings, based on Mendler-style

induction. This technique involves dispensing with dependent

induction, ensuring that datatypes can be lifted to predicates and

relying on relational formulations. A case study on proving subject

reduction for structural operational semantics illustrates that the

approach enables modular proofs, and that these proofs are essentially

similar to conventional ones.

Weak Completeness of Coalgebraic Dynamic Logics

The Arity Hierarchy in the Polyadic mu-Calculus

of nodes rather than just sets in labelled transition systems. It can express

exactly the polynomial-time computable and bisimulation-invariant queries on

finite graphs. In this paper we show that the hierarchy defined by fixing the arity

of formulas is strict, i.e. that higher arity yields greater expressive power. The

proof uses a diagonalisation argument.