Topics in Logic and Formal Methods in Computer Science

Assaf Kfoury

Spring 2006


There is a variety of logics for formal reasoning in many different domains of computer science. Apart from classical first-order logic, most commonly taught in a standard course in mathematical logic, several others have a more direct bearing on computer science.  Among the latter are intuitionistic logic, modal logic, temporal logic, dynamic logic, Hoare logic, specification logic, separation logic, non-monotonic logic, affine logic, linear logic, and several variations of each of the preceding -- to name a few that have been invented by computer scientists in recent years, or have been the object of renewed interest because of applications in computer science.

During the Spring 2006 semester we will cover topics in modal logic and linear logic, in approximate equal parts. Time permitting, also based on audience interests, we may have brief introductions to separation logic and/or Hoare logic. Material will be drawn from two recent texts:
  1. "Modal Logic" by P. Blackburn, M. de Rijke and Y. Venema -- paperback book available at Amazon.com for $39.97.
  2. "Linear Logic" by Frank Pfenning -- lecture notes available in the CS Department office for about $10.00.
Students will take turns in making weekly presentations, drawn from the reading material, based on which they will get credit for the course.
Exercises For:
Topics Proposed to be Covered in the Book "Modal Logic":

Maintained by Assaf Kfoury
Created:  05.12.28
Modified: 06.04.16