Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.3 4.3bsd-beta 6/6/85; site ucbvax.BERKELEY.EDU
Path: utzoo!decvax!ittatc!dcdwest!sdcsvax!ucbvax!ailist
From: gideon%edai.edinburgh.ac.uk@CS.UCL.AC.UK (Gideon Sahar)
Newsgroups: mod.ai
Subject: Seminar - Logics of Programmes (Edinburgh)
Message-ID: <Wed.Feb..5.12:20:32.1986.@.edai.edinburgh.ac.uk>
Date: Wed, 5-Feb-86 07:20:32 EST
Article-I.D.: .Wed.Feb..5.12:20:32.1986.
Posted: Wed Feb  5 07:20:32 1986
Date-Received: Sun, 9-Feb-86 01:24:15 EST
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The ARPA Internet
Lines: 24
Approved: ailist@sri-ai.arpa

From: Gideon Sahar <gideon%edai.edinburgh.ac.uk@cs.ucl.ac.uk>

			EDINBURGH AI SEMINARS

Date:		5th February 1986
Time:		2pm
Place:		Department of Artificial Intelligence
		Forrest Hill Seminar Room


Dr. D.C. McCarty, Center for Cognitive Sciences, University of Edinburgh,
will give a seminar entitled - `Logics of Programmes: Some Constructive
Comments'.


The talk will give an introduction to and overview of the applications of
constructive logic to programme verification. Three topics will be of
interest: the idea that functional interpretations of constructive set
theory are `high level' compilers; the relations between constructive
logic and Reynolds' `specification logic'; and the use of a constructive
meta theory in giving completeness proofs for hoare-style logics. We
will pre-suppose only a basic knowledge of mathematical logic; the
requisite technicalities from constructive logic and programme verification
will be explained in the talk.