A synergy between model-checking and type inference for the verification of value-passing higher-order processes

Abstract

In this paper, we present a formal verification framework for higher-order value-passing process algebra. This framework stems from an established synergy between type inference and model-checking. The language considered here is based on a sugared version of an implicitly typed λ-calculus extended with higher-order synchronous concurrency primitives. First, we endow such a syntax with a semantic theory made of a static semantics together with a dynamic semantics. The static semantics consists of an annotated type system. The dynamic semantics is operational and comes as a two-layered labeled transition system. The dynamic semantics is abstracted into a transitional semantics so as to make finite some infinite-state processes. We describe the syntax and the semantics of a verification logic that allows one to specify properties. The logic is an extension of the modal µ-calculus for handling higher-order processes, value-passing and return of results.