Symbolic Computation Group

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.

Another facet which we are actively exploring is the mismatch between the ``mathematics process'' and current tool support. While many parts of the mathematics process is well supported by various tools, no tool comes even close to offering a reasonable environment for ``doing mathematics''. As our main source of requirements, we use applications of mathematics to (formal) software engineering as well as to analysis (i.e. calculus). From our experience, these are two areas where new tools could have a large impact.