Virtue of certified programming with decision procedures

Add to your list(s) Download to your calendar using vCal

• Vladimir Komendantsky (St Andrews)
• Friday 25 May 2012, 11:00-12:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

NB: unusual day/time

In this moderately technical talk, I will discuss explicit termination of computations certified in Coq, and recall the importance of correct decision procedures for constructive understanding of computational problems. I will refer to examples of first-order definable relations on finite-state transition systems to show how logical analysis can underpin different degrees of type dependencies.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.