Symbolic Computation Group
David R. Cheriton School of Computer Science


Friday, May 29, 2009, at U. of Waterloo.
Abstract:
Doing mathematics by computer has divided into two camps: numerical analysis
and symbolic computation, both with very different flavours. Strangely,
symbolic computation itself has split into two: theorem proving and
algebraic (exact) computation. These two have developed largely
independently for the last 40 years [yes, that long]. But there is a subset
of these two communities who are striving to merge these two strands. Along
with William M. Farmer, we are implementing a new system which gives equal
weight to proofs and computation. Unlike our communities of origin, we value
both correctness and efficiency equally. We are using modern techniques
(partial evaluation, dependent types, abstract interpretation, generative
programming, etc) as part of our ``basic'' toolkit.

Last modified on Sunday, 04 November 2012, at 15:42 hours.