Lukas Convent: Bachelor's Thesis

Saarland University Computer Science

Compositional and Nameless Formalization of HOcore

Advisor: Tobias Tebbi

Abstract:

The focus of this thesis lies on better formalization techniques for the higher-order process calculus HOcore.

HOcore allows different definitions of bisimilarity. They are usually given in a compositional manner, however, proofs about HOcore in the literature do not make use of their compositional structure. Looking at bisimilarity from a coinductive perspective, we follow the work of Damien Pous by using his notion of compatible functions to achieve compositional proofs for the soundness of up-to techniques and for closure properties of bisimilarity. As some closure properties of components depend on one another, we introduce the notion of conditional closedness as a criterion applicable to bisimilarities respecting these dependencies. Using de Bruijn indices, we avoid any side-conditions about disjointness of free variables. We introduce transitions which produce a context for each unguarded variable. By this means, we can analyze transitions of substituted processes in an elegant way, avoiding structural congruence and the separate treatment of guarded and unguarded variables.

We apply these techniques to HOcore and show soundness of the up-to-bisimilarity technique as well as substitutivity and congruence of IO bisimilarity. The resulting proof architecture, which is formalized in the proof assistant Coq, provides a better understanding of the different components and their dependencies.

References

Thesis

Coq Development

Presentations


Lukas Convent, Wed Aug 17 12:54:35 2016