Lukas Convent: Bachelor's Thesis
Compositional and Nameless Formalization of HOcore
Advisor: Tobias Tebbi
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)
Coq Development
Presentations

Initial Seminar Talk: Slides (March 18, 2016)

Second Seminar Talk: Slides (May 13, 2016)

Final Talk: Slides (July 29, 2016)
Lukas Convent,
Wed Aug 17 12:54:35 2016