ENTCS
2008
14 years 15 days ago
2008
We introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-Binders calculus. Our analysis of a system is able to ...
ENTCS
2008
14 years 15 days ago
2008
We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a...
ENTCS
2008
14 years 15 days ago
2008
A category with biproducts is enriched over (commutative) additive monoids. A category with tensor products is enriched over scalar multiplication actions. A symmetric monoidal ca...
ENTCS
2008
14 years 15 days ago
2008
Abstract. We give a method of constructing an interpolant for linear equality, and inequality constraints over the rational numbers. Our method is based on efficient rewriting tech...
ENTCS
2008
14 years 15 days ago
2008
This paper presents fixpoint calculations on lattice structures as example of highly modular programming in a dependently typed functional language. We propose a library of Coq mo...
ENTCS
2008
14 years 15 days ago
2008
ENTCS
2008
14 years 15 days ago
2008
An algorithm to decide the emptiness of a regular type expression with set operators given a set of parameterized type definitions is presented. The algorithm generalizes previous...
ENTCS
2008
14 years 15 days ago
2008
In seeking a unified study of computational effects, in particular in order to give a general operational semantics agreeing with the standard one for state, one must take account...
ENTCS
2008
14 years 15 days ago
2008
As an extension to Floyd-Hoare logic, separation logic has been used to facilitate reasoning about imperative programs manipulating shared mutable data structures. Recently, it ha...
ENTCS
2008
14 years 15 days ago
2008
This paper explores a unification of the ideas of Concurrent Separation Logic with those of Communicating Sequential Processes. It extends separation logic by an operator for sepa...