From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/650
Path: news.gmane.org!not-for-mail
From: esik@inf.u-szeged.hu
Newsgroups: gmane.science.mathematics.categories
Subject: (unknown)
Date: Sun, 15 Feb 98 12:43 MET
Message-ID: <199802151144.HAA09888@mailserv.mta.ca>
NNTP-Posting-Host: main.gmane.org
X-Trace: ger.gmane.org 1241017096 26710 80.91.229.2 (29 Apr 2009 14:58:16 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 14:58:16 +0000 (UTC)
To: categories@mta.ca
Original-X-From: cat-dist Sun Feb 15 11:18:58 1998
Original-Received: (from Majordom@localhost)
	by mailserv.mta.ca (8.8.8/8.8.8) id KAA06607
	for categories-list; Sun, 15 Feb 1998 10:08:33 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Original-Sender: cat-dist@mta.ca
Precedence: bulk
Original-Lines: 36
Xref: news.gmane.org gmane.science.mathematics.categories:650
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/650>

>>From esik Sun Feb 15 12:43:53 +0100 1998 remote from inf.u-szeged.hu
To: categories@mta.ca
cc: esik
Subject: CATS Re: Categorical model for Floyd-Hoare logic
Date: Sun, 15 Feb 1998 12:43:53 +0100
From: Esik Zoltan <esik@inf.u-szeged.hu>
Received: from inf.u-szeged.hu by inf.u-szeged.hu; Sun, 15 Feb 1998 12:43 MET
Content-Type: text
Content-Length: 561


> Has there been work on a categorical model for 
> "while programs" (or,equivalently, assembly 
> language) and Floyd-Hoare logic?


The books

E.G. Manes: Predicate Transformer Semantics,
Cambridge University Press, 1992 

S.L. Bloom and Z. Esik: Iteration theories, 
Springer, 1993 (see in particular chapter 12
and 14)

and the paper

S.L. Bloom and Z. Esik: Floyd-Hoare logic 
in iteration theories, JACM, 38(1991), 887--934

consider such models. The books also contain 
references to other papers (including 
papers by Elgot and others). 

Zoltan Esik