Newsgroups: ut.theory
Path: utzoo!utgpu!jarvis.csri.toronto.edu!neat.ai.toronto.edu!bmkapron
From: bmkapron@theory.utoronto.ca (Bruce Kapron)
Subject: Student Seminar
Message-ID: <89Mar27.100902est.38215@neat.ai.toronto.edu>
Organization: Department of Computer Science, University of Toronto
Distribution: ut
Date: Mon, 27 Mar 89 10:09:01 EST

Once again, Arvind's talk will be postponed for a week. This week, Andrew
Malton will be presenting his ``interview'' talk.

Time: Tuesday, March 28, 3pm

Location: GB420

Title: A Type-Theoretic Explanation of Program Derivation

Description: Looking at the actual requirements of specification, and
the need to be able to complain when an implementation fails, I use
an idea of Godel to define specification, implementation, and complaint.
The result is a new interpretation of program specification connectives.
I then sketch how ordinary proofs of correctness (in Hoare's Logic)
represent implementations of such specifications.