[Agda] DoCon-A-2.00 announce

[Sergei Meshveliani]

                   A N N O U N C E M E N T

         DoCon-A  a Provable Algebraic Domain Constructor  

                       Version 2.00

is available, together with its source program and manual, 
on the Web at the following addresses:

  http://www.botik.ru/pub/local/Mechveliani/docon-A/    (Russian site),
  ftp.botik.ru/pub/local/Mechveliani/docon-A/           (same site),


DoCon-A is
----------
a  Computer Algebra library  written in a purely functional, non-strict 
language  Agda  having dependent types and allowing machine-checked
proofs.

DoCon-A applies generic programming. It defines generic notions of the 
algebraic structures: Semigroup, Group, Ring, and so on.
Arithmetic and some other operations are defined under the very
generic assumptions: "over any group", "over any ring", and so on.

Currently the following  Domain Constructors are supported (to a
certain 
extent): 
  Natural, Integer, Product, Fraction, Univariate Polynomial, 
  Euclidean Residue ring.

That is certain set of operations are defined automatically, following
these domain constructors. 


What is new with respect to previous version
--------------------------------------------

1. The representation of the generic algebra structures is simplified: 
   there are no `up'-structures. This makes the library design more
close to Standard library. 
           
2. The Field instance for Fraction domain over any unique factorization
ring, with certified optimized methods for arithmetic.         
   
3. Certain special equational provers InMonoid, InSemiringWithOne,
   InCommutativeSemiring are implemented  
   (something like a variant of RingSolver of Standard).       

   
Ports:    
------    
DoCon-A-2.00  has been tested under  
              Agda-2.5.3, MAlonzo, ghc-7.10.2, Linux.

Reports about possible later ports is in the current notes in the 
distribution:  
              notes/2.00.txt

Documentation.   See  manual.pdf.
-------------

Memory requirement 
------------------
For  Agda-2.5.3, ghc-7.10.2,  
and -M11G option (11G byte heap restriction) type-checking the library 
takes about 55 minutes on a 3 GHz computer.


The remarks are welcome:   mechvel at botik.ru