Abstract. This paper develops a highly expressive semantic framework for program refinement that supports both temporal reasoning and reasoning about the knowledge of a single agen...
We relate several models of concurrency introduced in the literature in order to extend classical Mazurkiewicz traces. These are mainly Droste's concurrent automata and Arnold...
A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constru...
Furio Honsell, John Longley, Donald Sannella, Andr...