COMP 527: Logic and Computation

The course will follow to a large extent the course notes from Frank Pfenning on Constructive Logic(CL) and on Automated Theorem proving(ATP). Both course notes are available in pdf-format. We will post more detailled notes on WebCT.

- Formal Proof -- Theory and Practice , John Harrison, Notices of the AMS, Nov 2008.
- How to (really) trust a mathematical proof, Julie Rehmeyer, ScienceNews, Nov 2008
- A nice high-level summary and background to this course can be found in the article "Proofs are Programs: 19th Century Logic and 21st Century Computing", Phil Wadler, which appeared in Dr Dobbs Journal, special supplement on Software in the 21st century, December 2000.
- What in the name of Euclid is going on here?, Science
- Proof and Beauty, Economist, Mar 31, 2005
- The QED Manifesto, appeared in "Automated Deduction - CADE 12", Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994.
- Wolfgang Thomas: Logic for Computer Science:The Engineering Challenge
- J. Halpern, R. Harper, N. Immerman, P. Kolaitis, M. Y. Vardi, V. Vianu: On the Unusual effectiveness of Logic in Computer Science
- NSF/CISE Workshop on The Unusual Effectiveness of Logic in Computer Science, National Science Foundation, 2001
- Michael Huth, Logic in Computer Science:tool-based modeling and reasoning about systems,Proceedings of the International Conference on Frontiers in Education 2000, Kansas City, October 2000.