Speaker / Predavač :

Petar Maksimović
Matematičkom Institutu SANU Beograd
INRIA Rennes, France

Title / Naslov:

A Core Calculus for Higher-Order Process Calculi and its Formalization in Coq

Abstract / Abstrakt:

HOCore is a minimal higher-order process calculus that features input-prefixed processes, output processes, and parallel composition. While it is Turing-complete, its observational equivalence remains decidable. Furthermore, the main forms of strong bisimilarity considered in the literature (contextual equivalence, barbed congruence, higher-order bisimilarity, context bisimilarity, and normal bisimilarity) all coincide in HOCore. Moreover, their synchronous and asynchronous versions coincide as well. It is thus possible to decide that two processes are equivalent, yet it is impossible, in the general case, to decide whether they terminate. We present a formal proof of these properties in the proof assistant Coq and discuss the imprecisions revealed, errors corrected, and insights gained through this formalization.

O predavaču:
Petar Maksimović je doktorirao 2013. godine na Fakultetu tehničkih nauka u Novom Sadu i na Univerzitetu u Nici Sophia Antipolis u Francuskoj, u okviru zajedničkih doktorskih studija. Zaposlen je na Matematičkom Institutu u Beogradu, a trenutno je na jednogodišnjem usavršavanju u Francuskoj, u istrazivačkom centru INRIA Rennes - Bretagne Atlantique.