Pict Correctness Revisited

The Pict programming language is an implementation of the π-calculus in which executions of π-calculus terms are specified via an abstract machine. An important property of any concurrent programming language implementation is the fair execution of threads. After defining fairness for the π-calculus, we show that Pict abstract machine executions implement fair π-calculus executions. We also give new proofs of s and liveness for the Pict abstract machine.

• Type: Conference
• Year: 2007
• Where: FMOODS
• Authors: Philippe Bidinger, Adriana B. Compagnoni
• Keywords: FMOODS 2007, Formal Methods, Machine Executions Implement, Pict Abstract Machine, Pict Programming Language