Program Semantics and Classical Logic

• We have taken the naive view that the meaning of a program consists
in a relation between input and output states. But more finegrained
notions of meaning (for example, the meaning of a program as a process
or as an execution trace) do not seem to be in conflict with the methods
employed here. As long as we let programs be translated as terms of
relational type the methods of section 7 seem to be applicable.

References

[1] P.B. Andrews. An Introduction to Mathematical Logic and Type Theory:
to Truth through Proof. Academic Press, Orlando, Florida, 1975.

[2] A. Church. A Formulation of the Simple Theory of Types. Journal of
Symbolic Logic, 5:56-68, 1940.

[3] J. De Bakker. Mathematical Theory of Program Correctness. Prentice-
Hall, Englewood Cliffs, NJ, 1980.

[4] D. Gallin. Intensional and Higher-Order Modal Logic. North-Holland,
Amsterdam, 1975.

[5] R. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes,
Stanford, 1987.

[6] J. Groenendijk and M. Stokhof. Dynamic Montague Grammar. In
L. Kalman and L. Polos, editors, Papers from the Second Symposium
on Logic and Language, pages 3-48. Akademiai Kiado, Budapest, 1990.

[7] D. Harel. Dynamic Logic. In D.M. Gabbay and F. Guenthner, edi-
tors, Handbook of Philosophical Logic, volume II, pages 497-604. Reidel,
Dordrecht, 1984.

[8] L. Henkin. Completeness in the Theory of Types. Journal of Symbolic
Logic, 15:81-91, 1950.

[9] L. Henkin. A Theory of Propositional Types. Fundamenta Mathemati-
cae, 52:323-344, 1963.

[10] Th. Janssen. Foundations and Applications of Montague Grammar. Cen-
tre for Mathematics and Computer Science, Amsterdam, 1986.

31

<<   28   29   30   31   32   33   >>

More intriguing information