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.