[mod.ai] Seminar - Logics of Programmes

gideon%edai.edinburgh.ac.uk@CS.UCL.AC.UK (Gideon Sahar) (02/05/86)

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.