In this paper we propose an efficient algorithmic solution to the problem of determining a Bisimulation Relation on a finite structure. Starting from a set-theoretic point of view we propose an algorithm that optimizes the solution to the Relational …
We present a logical framework for reasoning on a very general class of languages featuring binding operators, called nominal algebras, presented in higher-order abstract syntax (HOAS). is based on an axiomatic syntactic standpoint and it consists of …
In this paper we develop a new method for solving queries on semistructured data. The main idea is to see a database as a Kripke Transition System (a model) and a query as a formula of the temporal logic CTL. In this way, the retrieval of data …
We present two case studies in formal reasoning about untyped λ-calculus in Coq, using both first-order and higher-order abstract syntax. In the first case, we prove the equivalence of three definitions of α-equivalence; in the second, we focus on …
In this paper we consider the relative expressive power of two very common operators applicable to sets and multisets: the with and the union operators. For such operators we prove that they are not mutually expressible by means of existentially …