The Coq mailing list

[Randy Pollack <rap AT dcs.ed.ac.uk>]

To seriously consider suitability of logics for computer science, you
should consider strictly finitistic frameworks too.

Sure, every program in (for example) Type Theory terminates, but that
is more a logical point (the logic is consistent) that a computer
science point.  For actually running programs, termination is no
information at all.  A logic that gives bounds is useful for computer
science.

Best,
Randy
-------------------------------
Amy Felty writes:
 >   Does anyone have any suggestions for readings that address the
 >   following question?:
 > 
 >   "In what sense logics that are used in computer
 >   science are more likeley to be intuitionistic, having
 >   in mind that  classical logics have also been used.
 >   What are the advantages and disadvangates of using
 >   classical logic in computer science application?"
 > 
 > I am submitting this question for a Philosophy graduate student here at
 > the University of Ottawa.  Please include her (Mehrnoosh Sadrzadeh, email:
 > mehrnoosh_sadr AT yahoo.com)
 >  in your replies.  Thank you very much.
 > 
 > Amy Felty
 > 
 > 
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club