Atypical: Integrating computer algebra and reasoning

Simon Thompson, John Shackell, James Beaumont and Leonid Timochouk

This is the home page for the project Integrating Computer Algebra and Reasoning: Incorporating a logic into the Aldor system, funded under EPSRC Grant GR/M37851.

The project

Understanding the Aldor compiler

Adding type annotations to Aldor programs.
Report on the Aldor compiler Chris Ryder.
The Type System of Aldor. Erik Poll and Simon Thompson. Technical Report 11-99.

Project publications

Adding the Axioms to Axiom: a paper presented at the Calculemus and Types workshop, Eindhoven, July 1998.
Integrating Computer Algebra and Reasoning through the Type System of Aldor. Erik Poll and Simon Thompson. From Frontiers of Combining Systems: Frocos 2000, LNCS 1794, 2000.
Logic and Dependent Types in the Aldor Computer Algebra System and the programs from the document.
Asymptotic Expansions with Oscillating Coefficients Bruno Salvy and John Shackell.
Complexity bounds for zero-test algorithmsJohn Shackell and Joris van der Hoeven.
The Aldor-- Language Simon Thompson and Leonid Timochouk.
- Logic in Aldor--: NewPropLogic.as.
- Commutative monoid in Aldor--: CommMonoid.as.

The Aldor-- system

Download the tarball.
Please mail Simon Thompson to receive a binary distribution of the modified Aldor compiler.
Using the AETHER system.

Last modified 07.01.03