Archive for the 'Pi-calculus' Category

A name abstraction functor for named sets

By Vincenzo Ciancia and Ugo Montinari, from CMCS 2008, available from Vincenzo Ciancia’s website:

The problem of dening fully abstract operational models of name passing calculi has been given some elegant solutions, such as coalgebras over presheaf categories or over nominal sets. These formalisms fail to model garbage collection of unused names, hence they do not have nice properties with respects to finite state algorithms. The category of named sets, on the other hand, was designed for the purpose of supporting ecient algorithms to handle the semantics of name passing calculi. However the theory was developed in a rather ad-hoc fashion (e.g. the existence of a final coalgebra was only proved in the finite case). In this work we introduce a name abstraction functor for named sets and show that it provides a simple and effective notion of garbage collection of unused names. Along the way, we survey a number of needed results on the category of permutation algebras, an algebra-theoretic denition of nominal sets. In particular we give a formalization of the adjunction between abstraction and concretion, an example illustrating a nominal syntax alike handling of De Bruijn indexes, and an explicit functor to model the early semantics of the π -calculus in nominal sets.

Advertisements

Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts

By Christine Roeckl, Daniel Hirchskoff and Stefan Berghofer, from FOSSACS 2001, available from Christine Roeckl’s website:

Higher-order abstract syntax is a natural way to formalize programming languages with binders, like the pi-calculus, because alpha-conversion, instantiations and capture avoidance are delegated to the meta-level of the provers, making tedious substitutions superfluous. However, such formalizations usually lack structural induction, which makes syntax-analysis impossible. Moreover, when applied in logical frameworks with object logics, like Isabelle/HOL or standard extensions of Coq, exotic terms can be defined, for which important syntactic properties become invalid.

The paper presents a formalization of the pi-calculus in Isabelle/HOL, using well-formedness predicates which both eliminate exotic terms and yield structural induction. These induction-principles are then used to derive the Theory of Contexts fully within the mechanization.

Proof scripts are available here.