<%@ page language="java" contentType="text/html" %> <%-- Include common initialisation code --%> <%@ include file="/arch/common.jsp" %> <%-- The current tab --%> <% String currentTab = "Research"; %> <%-- Content of navigation pane --%> <%@ include file="nav.jsp" %> <% showCurrentLink=true; %> <%-- Current navigation location --%> <% String currentNav = "Reports and Theses"; %> <%-- Include the code for the document header --%> <%@ include file="/arch/header.jsp" %>

Research Report CS-RR-251

<%-- Include the code for the lines and navigation --%> <%@ include file="/arch/middle.jsp" %>

S.G. Matthews, An Extensional Treatment of Lazy Data Flow Deadlock (October 1, 1993).

Abstract

In An Extensional Treatment of Dataflow Deadlock [Wa81] Wadge introduced an elegant non operational test for proving that many of Kahn's data flow message passing networks [Ka74] must be free of deadlock; a test that "should extend to a much wider context" in the study of program correctness. Such a context has now been provided with the introduction of partial metric spaces [Ma92]. These spaces can be used to describe semantic domains such as those used in lazy data flow languages [W &A85]. This paper develops Wadge's ideas on establishing an extensional theory of program correctness by using partial metric spaces to give a non operational treatment of lazy data flow deadlock.

<%@ include file="cited.html" %>

S.G. Matthews, "The Cycle Contraction Mapping Theorem", Theoretical Computer Science 151, pp. 195-205 (1995)

<%-- Include the code for the document footer --%> <%@ include file="/arch/footer.jsp" %>