Compositional and Nameless Formalization of HOcore
Advisor: Tobias Tebbi
Supervisor: Prof. Dr. Gert Smolka
Abstract
The focus of this thesis lies on better formalization techniques for the higherorder 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 upto 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 sideconditions 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 uptobisimilarity 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

Explicit substitutions (1991)
Martín Abadi, Luca Cardelli, PierreLouis Curien, and JeanJacques Lévy 
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the ChurchRosser theorem (1972)
Nicolaas Govert De Bruijn 
A full formalisation of picalculus theory in the calculus of constructions (1997)
Daniel Hirschkoff 
The power of parameterization in coinductive proof (2013)
ChungKil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis 
Coq formalization of the higherorder recursive path ordering (2009)
Adam Koprowski 
On the expressiveness and decidability of higherorder process calculi (2011)
Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt 
HOCore in Coq (2015)
Petar Maksimović and Alan Schmitt 
Communication and concurrency (1989)
Robin Milner 
A calculus of mobile processes, I (1992)
Robin Milner, Joachim Parrow, and David Walker 
Higherorder psicalculi (2014)
Joachim Parrow, Johannes Borgström, Palle Raabjerg, and Johannes Åman Pohjola 
Complete lattices and upto techniques (2007)
Damien Pous 
Coinduction all the way up (2016)
Damien Pous 
Expressing mobility in process algebras: firstorder and higherorder paradigms (1993)
Davide Sangiorgi 
On the bisimulation proof method (1998)
Davide Sangiorgi 
Autosubst: Reasoning with de
Bruijn terms and parallel substitutions (2015)
Steven Schäfer, Tobias Tebbi, and Gert Smolka 
Introduction to computational logic.
Lecture Notes (2014)
Gert Smolka and Chad E. Brown 
A latticetheoretical fixpoint theorem and its applications (1955)
Alfred Tarski 
Nominal techniques in Isabelle/HOL (2008)
Christian Urban
Thesis
 Thesis (submitted August 17, 2016)