Lukas Convent: Bachelor's Thesis

Programming Systems

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 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

• Explicit substitutions (1991)
  Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)
  Nicolaas Govert De Bruijn
• A full formalisation of pi-calculus theory in the calculus of constructions (1997)
  Daniel Hirschkoff
• The power of parameterization in coinductive proof (2013)
  Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis
• Coq formalization of the higher-order recursive path ordering (2009)
  Adam Koprowski
• On the expressiveness and decidability of higher-order 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
• Higher-order psi-calculi (2014)
  Joachim Parrow, Johannes Borgström, Palle Raabjerg, and Johannes Åman Pohjola
• Complete lattices and up-to techniques (2007)
  Damien Pous
• Coinduction all the way up (2016)
  Damien Pous
• Expressing mobility in process algebras: first-order and higher-order 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 lattice-theoretical fixpoint theorem and its applications (1955)
  Alfred Tarski
• Nominal techniques in Isabelle/HOL (2008)
  Christian Urban

Thesis

• Thesis (submitted August 17, 2016)

Coq Development

• Download Coq proof scripts
• Browse Coqdoc documentation

Presentations

• Initial Seminar Talk: Slides (March 18, 2016)
• Second Seminar Talk: Slides (May 13, 2016)
• Final Talk: Slides (July 29, 2016)