diff --git a/halg-core-test/halg-core-test.cabal b/halg-core-test/halg-core-test.cabal
index 23202b47..ae4cd340 100644
--- a/halg-core-test/halg-core-test.cabal
+++ b/halg-core-test/halg-core-test.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 9e31175e35b0b93f2f915aa2ec9fcd5a447c3a05722120d942aa470640d42279
+-- hash: 2775958dc78ed62c1a1ec0e22067ce1381c763d699bb7bdd0a3e3095bb179b02
 
 name:           halg-core-test
 version:        0.1.0.0
@@ -53,6 +53,7 @@ library
       Algebra.Field.Finite.Test
       Algebra.Field.Fraction.Test
       Algebra.Field.Prime.Test
+      Algebra.Ring.Euclidean.Quotient.Test
       Algebra.Ring.Ideal.Test
       Algebra.Ring.Polynomial.Monomial.Test
       Algebra.Ring.Polynomial.Test
diff --git a/halg-core-test/src/Algebra/Ring/Euclidean/Quotient/Test.hs b/halg-core-test/src/Algebra/Ring/Euclidean/Quotient/Test.hs
new file mode 100644
index 00000000..efd8f9eb
--- /dev/null
+++ b/halg-core-test/src/Algebra/Ring/Euclidean/Quotient/Test.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE PolyKinds #-}
+
+module Algebra.Ring.Euclidean.Quotient.Test () where
+
+import Algebra.Ring.Euclidean.Quotient
+import AlgebraicPrelude (Euclidean)
+import Data.Reflection
+import Test.QuickCheck
+
+instance
+  (Euclidean a, Arbitrary a, Reifies s a) =>
+  Arbitrary (Quotient s a)
+  where
+  arbitrary = quotient <$> arbitrary
diff --git a/halg-core-test/src/Algebra/TestUtils.hs b/halg-core-test/src/Algebra/TestUtils.hs
index e896af67..27b72f90 100644
--- a/halg-core-test/src/Algebra/TestUtils.hs
+++ b/halg-core-test/src/Algebra/TestUtils.hs
@@ -33,10 +33,13 @@ import qualified Test.QuickCheck as QC
 import Test.QuickCheck.Instances ()
 import Prelude (($))
 
-liftSNat :: (forall n. KnownNat (n :: Nat) => SNat n -> Property) -> Natural -> Property
+liftSNat :: (forall n. KnownNat (n :: Nat) => SNat n -> x) -> Natural -> x
 liftSNat f i =
   case toSomeSNat i of
     SomeSNat sn -> withKnownNat sn $ f sn
 
-checkForTypeNat :: [Natural] -> (forall n. KnownNat (n :: Nat) => SNat n -> Property) -> Property
+checkForTypeNat ::
+  [Natural] ->
+  (forall n. KnownNat (n :: Nat) => SNat n -> Property) ->
+  Property
 checkForTypeNat as test = forAll (QC.elements as) $ liftSNat test
diff --git a/halg-core/src/Algebra/Ring/Euclidean/Quotient.hs b/halg-core/src/Algebra/Ring/Euclidean/Quotient.hs
index f8fdead5..61afa981 100644
--- a/halg-core/src/Algebra/Ring/Euclidean/Quotient.hs
+++ b/halg-core/src/Algebra/Ring/Euclidean/Quotient.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
diff --git a/halg-polynomials/halg-polynomials.cabal b/halg-polynomials/halg-polynomials.cabal
index f6f6565d..d79a6ad3 100644
--- a/halg-polynomials/halg-polynomials.cabal
+++ b/halg-polynomials/halg-polynomials.cabal
@@ -36,6 +36,7 @@ library
       Algebra.Prelude.Core
       Algebra.Ring.Polynomial
       Algebra.Ring.Polynomial.Labeled
+      Algebra.Ring.Polynomial.List
       Algebra.Ring.Polynomial.Quotient
       Algebra.Ring.Polynomial.Univariate
   other-modules:
@@ -74,6 +75,7 @@ library
     , reflection
     , singletons-presburger
     , sized
+    , strict
     , text
     , type-natural
     , unamb
@@ -92,11 +94,13 @@ test-suite halg-polynomials-spec
   type: exitcode-stdio-1.0
   main-is: Spec.hs
   other-modules:
-      GroebnerSpec
-      PolynomialSpec
-      UnivariateSpec
-      QuotientSpec
+      Algebra.Algorithms.GroebnerSpec
+      Algebra.Ring.Polynomial.ListSpec
+      Algebra.Ring.Polynomial.QuotientSpec
+      Algebra.Ring.Polynomial.UnivariateSpec
+      Algebra.Ring.PolynomialSpec
       Utils
+      Paths_halg_polynomials
   hs-source-dirs:
       test
   default-extensions:
@@ -112,6 +116,8 @@ test-suite halg-polynomials-spec
       TypeInType
       UndecidableInstances
   ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N
+  build-tool-depends:
+      tasty-discover:tasty-discover
   build-depends:
       QuickCheck
     , algebra
@@ -121,9 +127,11 @@ test-suite halg-polynomials-spec
     , halg-core
     , halg-core-test
     , halg-polynomials
-    , hspec
-    , hspec-discover
     , matrix
     , sized
+    , tasty
+    , tasty-expected-failure
+    , tasty-hunit
+    , tasty-quickcheck
     , vector
   default-language: Haskell2010
diff --git a/halg-polynomials/package.yaml b/halg-polynomials/package.yaml
index 9a19ec54..66c9b3f6 100644
--- a/halg-polynomials/package.yaml
+++ b/halg-polynomials/package.yaml
@@ -58,6 +58,7 @@ library:
   - deepseq
   - equational-reasoning
   - ghc-typelits-knownnat
+  - strict
   - singletons-presburger
   - hashable
   - heaps
@@ -100,23 +101,21 @@ tests:
   halg-polynomials-spec:
     main:                Spec.hs
     source-dirs:         test
-    other-modules:
-    - GroebnerSpec
-    - PolynomialSpec
-    - UnivariateSpec
-    - QuotientSpec
-    - Utils
     ghc-options:
     - -Wall
     - -threaded
     - -rtsopts
     - -with-rtsopts=-N
+    build-tools:
+    - tasty-discover
     dependencies:
     - QuickCheck
     - containers
     - halg-core-test
     - halg-polynomials
-    - hspec
-    - hspec-discover
+    - tasty
+    - tasty-expected-failure
+    - tasty-hunit
+    - tasty-quickcheck
     - matrix
     - vector
diff --git a/halg-polynomials/src/Algebra/Ring/Polynomial/List.hs b/halg-polynomials/src/Algebra/Ring/Polynomial/List.hs
new file mode 100644
index 00000000..2f87b5f9
--- /dev/null
+++ b/halg-polynomials/src/Algebra/Ring/Polynomial/List.hs
@@ -0,0 +1,407 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- | Multivariate polynomials, expressed as a list of terms with decreasing monomials.
+module Algebra.Ring.Polynomial.List
+  ( ListPoly (),
+
+    -- * Internal utility function for testing
+    isNormalForm,
+  )
+where
+
+import Algebra.Prelude.Core hiding (coerce)
+import Control.Arrow ((>>>))
+import Control.DeepSeq (NFData)
+import Control.Lens (alaf)
+import qualified Data.Bifunctor as Bi
+import Data.Coerce
+import qualified Data.HashSet as HS
+import Data.Kind (Type)
+import qualified Data.Map.Strict as M
+import qualified Data.Set as S
+import qualified Data.Sized as SV
+import Data.Strict (toLazy, toStrict)
+import Data.Strict.Tuple (Pair (..))
+import qualified Data.Strict.Tuple as STuple
+import GHC.Exts (proxy#)
+import qualified GHC.TypeLits as TL
+import Numeric.Algebra (Ring (fromInteger))
+import qualified Numeric.Algebra as A
+
+newtype ListPoly r (order :: Type) n = ListPoly {runListPoly :: [Pair r (OrderedMonomial order n)]}
+  deriving (Eq)
+  deriving (NFData) via [Pair r (OrderedMonomial order n)]
+
+deriving via
+  WrapAlgebra (ListPoly r order n)
+  instance
+    ( IsMonomialOrder n order
+    , KnownNat n
+    , Ring r
+    , CoeffRing r
+    , UnitNormalForm r
+    ) =>
+    Num (ListPoly r order n)
+
+deriving instance
+  (Eq r, Ord r, IsMonomialOrder n order) =>
+  Ord (ListPoly r order n)
+
+instance
+  (CoeffRing r, UnitNormalForm r, KnownNat n, IsMonomialOrder n order) =>
+  UnitNormalForm (ListPoly r order n)
+  where
+  splitUnit = splitUnitDefault
+
+instance
+  ( CoeffRing r
+  , UnitNormalForm r
+  , KnownNat n
+  , IsMonomialOrder n order
+  ) =>
+  DecidableAssociates (ListPoly r order n)
+  where
+  isAssociate = isAssociateDefault
+  {-# INLINE isAssociate #-}
+
+instance
+  (CoeffRing r, ZeroProductSemiring r, KnownNat n, IsMonomialOrder n order) =>
+  ZeroProductSemiring (ListPoly r order n)
+
+instance
+  ( CoeffRing r
+  , KnownNat n
+  , IsMonomialOrder n order
+  , Field r
+  ) =>
+  IntegralDomain (ListPoly r order n)
+  where
+  p `divides` q = isZero $ p `modPolynomial` [q]
+  {-# INLINE divides #-}
+  p `maybeQuot` q =
+    if isZero q
+      then Nothing
+      else
+        let (r, s) = p `divModPolynomial` [q]
+         in if isZero s
+              then Just $ snd $ head r
+              else Nothing
+  {-# INLINE maybeQuot #-}
+
+instance
+  (CoeffRing r, IsMonomialOrder n order, DecidableUnits r, KnownNat n) =>
+  DecidableUnits (ListPoly r order n)
+  where
+  isUnit = isUnitDefault
+  recipUnit = recipUnitDefault
+
+mergePolyWith ::
+  forall n order r s t.
+  (IsMonomialOrder n order, DecidableZero t) =>
+  (r -> s -> t) ->
+  (r -> t) ->
+  (s -> t) ->
+  ListPoly r order n ->
+  ListPoly s order n ->
+  ListPoly t order n
+{-# INLINE mergePolyWith #-}
+mergePolyWith mg inl inr = coerce loop
+  where
+    loop ::
+      [Pair r (OrderedMonomial order n)] ->
+      [Pair s (OrderedMonomial order n)] ->
+      [Pair t (OrderedMonomial order n)]
+    {-# INLINE loop #-}
+    loop [] rs = map (Bi.first inr) rs
+    loop ls [] = map (Bi.first inl) ls
+    loop ls@((c :!: mon) : ls') rs@((d :!: mon') : rs') =
+      case compare mon mon' of
+        LT -> (inr d :!: mon') : loop ls rs'
+        EQ ->
+          let !coe = mg c d
+           in if isZero coe
+                then loop ls' rs'
+                else (coe :!: mon) : loop ls' rs'
+        GT -> (inl c :!: mon) : loop ls' rs
+
+instance
+  (DecidableZero r, IsMonomialOrder n order) =>
+  Additive (ListPoly r order n)
+  where
+  (+) = mergePolyWith (+) id id
+  {-# INLINE (+) #-}
+
+instance
+  (DecidableZero r, IsMonomialOrder n order) =>
+  LeftModule Natural (ListPoly r order n)
+  where
+  n .* ListPoly xs
+    | n == 0 = ListPoly []
+    | otherwise =
+      ListPoly $ filter (not . isZero . STuple.fst) $ map (Bi.first (n .*)) xs
+  {-# INLINE (.*) #-}
+
+instance
+  (DecidableZero r, IsMonomialOrder n order) =>
+  RightModule Natural (ListPoly r order n)
+  where
+  ListPoly xs *. n
+    | n == 0 = ListPoly []
+    | otherwise =
+      ListPoly $ filter (not . isZero . STuple.fst) $ map (Bi.first (*. n)) xs
+  {-# INLINE (*.) #-}
+
+instance
+  (DecidableZero r, IsMonomialOrder n order) =>
+  Monoidal (ListPoly r order n)
+  where
+  zero = ListPoly []
+  {-# INLINE zero #-}
+
+instance
+  ( DecidableZero r
+  , Abelian r
+  , IsMonomialOrder n order
+  ) =>
+  Abelian (ListPoly r order n)
+
+instance
+  (DecidableZero r, LeftModule Integer r, IsMonomialOrder n order) =>
+  LeftModule Integer (ListPoly r order n)
+  where
+  n .* ListPoly xs
+    | n == 0 = ListPoly []
+    | otherwise =
+      ListPoly $ filter (not . isZero . STuple.fst) $ map (Bi.first (n .*)) xs
+  {-# INLINE (.*) #-}
+
+instance
+  (DecidableZero r, RightModule Integer r, IsMonomialOrder n order) =>
+  RightModule Integer (ListPoly r order n)
+  where
+  ListPoly xs *. n
+    | n == 0 = ListPoly []
+    | otherwise =
+      ListPoly $ filter (not . isZero . STuple.fst) $ map (Bi.first (*. n)) xs
+  {-# INLINE (*.) #-}
+
+instance
+  (DecidableZero r, Group r, IsMonomialOrder n order) =>
+  Group (ListPoly r order n)
+  where
+  (-) = mergePolyWith (-) id negate
+  {-# INLINE (-) #-}
+  negate = coerce $ map @[] (Bi.first @Pair @r @r @(OrderedMonomial order n) negate)
+  {-# INLINE negate #-}
+
+instance
+  (DecidableZero r, KnownNat n, Multiplicative r, IsMonomialOrder n order) =>
+  Multiplicative (ListPoly r order n)
+  where
+  l@(ListPoly []) * _ = l
+  _ * r@(ListPoly []) = r
+  ListPoly ls * ListPoly r =
+    alaf
+      Add
+      foldMap
+      ( \(o :!: m) ->
+          ListPoly
+            [ c' :!: (m * m')
+            | c :!: m' <- r
+            , let c' = o * c
+            , not $ isZero c'
+            ]
+      )
+      ls
+  {-# INLINE (*) #-}
+
+instance
+  ( DecidableZero r
+  , Semiring r
+  , KnownNat n
+  , IsMonomialOrder n order
+  ) =>
+  Semiring (ListPoly r order n)
+
+instance
+  ( DecidableZero r
+  , Unital r
+  , IsMonomialOrder n order
+  , KnownNat n
+  ) =>
+  Unital (ListPoly r order n)
+  where
+  one = ListPoly [one :!: one]
+
+instance
+  ( DecidableZero r
+  , Commutative r
+  , KnownNat n
+  , IsMonomialOrder n order
+  ) =>
+  Commutative (ListPoly r order n)
+
+instance
+  (DecidableZero r, IsMonomialOrder n order) =>
+  DecidableZero (ListPoly r order n)
+  where
+  isZero = null . runListPoly
+  {-# INLINE isZero #-}
+
+instance
+  (Semiring r, DecidableZero r, IsMonomialOrder n order) =>
+  LeftModule (Scalar r) (ListPoly r order n)
+  where
+  (.*) a =
+    coerce $
+      filter (not . isZero @r . STuple.fst)
+        . map @[]
+          ( Bi.first @Pair @r @r @(OrderedMonomial order n)
+              (runScalar a *)
+          )
+  {-# INLINE (.*) #-}
+
+instance
+  (Semiring r, DecidableZero r, IsMonomialOrder n order) =>
+  RightModule (Scalar r) (ListPoly r order n)
+  where
+  (*.) = flip $ \a ->
+    coerce $
+      filter (not . isZero @r . STuple.fst)
+        . map @[]
+          ( Bi.first @Pair @r @r @(OrderedMonomial order n)
+              (* runScalar a)
+          )
+  {-# INLINE (*.) #-}
+
+instance
+  (IsMonomialOrder n order, KnownNat n, Rig r, DecidableZero r) =>
+  Rig (ListPoly r order n)
+
+instance
+  (IsMonomialOrder n order, KnownNat n, Ring r, DecidableZero r) =>
+  Ring (ListPoly r order n)
+  where
+  fromInteger n =
+    let !c = A.fromInteger n
+     in if isZero c
+          then ListPoly []
+          else ListPoly [c :!: one]
+
+instance
+  (CoeffRing r, KnownNat n, IsMonomialOrder n order) =>
+  IsPolynomial (ListPoly r order n)
+  where
+  type Arity (ListPoly r order n) = n
+  type Coefficient (ListPoly r order n) = r
+  liftMap f =
+    alaf
+      Add
+      foldMap
+      ( \(c :!: OrderedMonomial mon) ->
+          Scalar c
+            .* runMult
+              ( ifoldMapMonom
+                  (\i p -> Mult $ f i ^ fromIntegral p)
+                  mon
+              )
+      )
+      . runListPoly
+  {-# INLINE liftMap #-}
+  monomials = HS.fromList . map (getMonomial . STuple.snd) . runListPoly
+  {-# INLINE monomials #-}
+  terms' = M.fromList . map (toLazy . STuple.swap) . coerce
+  {-# INLINE terms' #-}
+  sArity = const sNat
+  {-# INLINE sArity #-}
+  arity = const $ TL.natVal' @n proxy#
+  {-# INLINE arity #-}
+  injectCoeff c
+    | isZero c = ListPoly []
+    | otherwise = ListPoly [c :!: one]
+  {-# INLINE injectCoeff #-}
+  coeff' = coeff . OrderedMonomial
+  {-# INLINE coeff' #-}
+  constantTerm =
+    runListPoly >>> last >>> \(c :!: mon) ->
+      if mon == one
+        then c
+        else zero
+  {-# INLINE constantTerm #-}
+  fromMonomial = ListPoly . (: []) . (one :!:) . OrderedMonomial
+  {-# INLINE fromMonomial #-}
+  toPolynomial' = coerce $ toPolynomial @(ListPoly r order n)
+  {-# INLINE toPolynomial' #-}
+
+instance
+  (CoeffRing r, KnownNat n, IsMonomialOrder n order) =>
+  IsOrderedPolynomial (ListPoly r order n)
+  where
+  type MOrder (ListPoly r order n) = order
+  leadingTerm =
+    runListPoly
+      >>> \case
+        [] -> (zero, one)
+        tm : _ -> toLazy tm
+  {-# INLINE leadingTerm #-}
+  leadingCoeff =
+    runListPoly
+      >>> \case
+        [] -> zero
+        (c :!: _) : _ -> c
+  {-# INLINE leadingCoeff #-}
+  leadingMonomial =
+    runListPoly
+      >>> \case
+        [] -> one
+        (_ :!: mon) : _ -> mon
+  {-# INLINE leadingMonomial #-}
+  splitLeadingTerm =
+    runListPoly
+      >>> \case
+        [] -> ((zero, one), ListPoly [])
+        tm : rest -> (toLazy tm, ListPoly rest)
+  {-# INLINE splitLeadingTerm #-}
+  coeff mon =
+    runListPoly
+      >>> dropWhile ((> mon) . STuple.snd)
+      >>> \case
+        (c :!: mon') : _ | mon == mon' -> c
+        _ -> zero
+  {-# INLINE coeff #-}
+  toPolynomial tm@(c, _)
+    | isZero c = ListPoly []
+    | otherwise = ListPoly [toStrict tm]
+  {-# INLINE toPolynomial #-}
+  fromOrderedMonomial = ListPoly . (: []) . (one :!:)
+  {-# INLINE fromOrderedMonomial #-}
+  orderedMonomials = S.fromDescList . map STuple.snd . runListPoly
+  {-# INLINE orderedMonomials #-}
+  polynomial = ListPoly . filter (not . isZero . STuple.fst) . map (toStrict . swap) . M.toDescList
+  {-# INLINE polynomial #-}
+  mapMonomialMonotonic f = ListPoly . map (Bi.second f) . runListPoly
+  {-# INLINE mapMonomialMonotonic #-}
+
+instance
+  (PrettyCoeff r, CoeffRing r, KnownNat n, IsMonomialOrder n order) =>
+  Show (ListPoly r order n)
+  where
+  showsPrec = showsPolynomialWith $
+    SV.generate' $ \i ->
+      "X_" <> show (ordToNatural i)
+  {-# INLINE showsPrec #-}
+
+isNormalForm ::
+  (CoeffRing r, IsMonomialOrder n ord) =>
+  ListPoly r ord n ->
+  Bool
+isNormalForm (ListPoly ts) =
+  not (any (isZero . STuple.fst) ts)
+    && and (zipWith ((>) `on` STuple.snd) ts (drop 1 ts))
\ No newline at end of file
diff --git a/halg-polynomials/src/Algebra/Ring/Polynomial/Univariate.hs b/halg-polynomials/src/Algebra/Ring/Polynomial/Univariate.hs
index 01da5e25..9db5f1da 100644
--- a/halg-polynomials/src/Algebra/Ring/Polynomial/Univariate.hs
+++ b/halg-polynomials/src/Algebra/Ring/Polynomial/Univariate.hs
@@ -27,6 +27,9 @@ module Algebra.Ring.Polynomial.Univariate
     liftMapUnipol,
     module Algebra.Ring.Polynomial.Class,
     module Algebra.Ring.Polynomial.Monomial,
+
+    -- * Internal utilities
+    isNormalForm,
   )
 where
 
@@ -49,7 +52,7 @@ import qualified Prelude as P
    please consider using other represntation.
 -}
 newtype Unipol r = Unipol {runUnipol :: IM.IntMap r}
-  deriving (NFData, Foldable)
+  deriving (Eq, NFData, Foldable)
 
 type role Unipol representational
 
@@ -177,10 +180,6 @@ varUnipol :: Unital r => Ordinal 1 -> Unipol r
 varUnipol _ = Unipol $ IM.singleton 1 one
 {-# NOINLINE [1] varUnipol #-}
 
-instance (Eq r, DecidableZero r) => Eq (Unipol r) where
-  (==) = (==) `on` IM.filter (not . isZero) . runUnipol
-  (/=) = (/=) `on` IM.filter (not . isZero) . runUnipol
-
 instance (Ord r, DecidableZero r) => Ord (Unipol r) where
   compare = comparing runUnipol
   (<) = (<) `on` runUnipol
@@ -418,7 +417,7 @@ liftMapUnipol g f@(Unipol dic) =
    in foldr
         (\a b -> a .*. one + b * u)
         (IM.findWithDefault zero n dic .*. one)
-        [IM.findWithDefault zero k dic | k <- [0 .. n -1]]
+        [IM.findWithDefault zero k dic | k <- [0 .. n - 1]]
 {-# INLINE liftMapUnipol #-}
 
 substWithUnipol ::
@@ -433,7 +432,7 @@ substWithUnipol (|*) g f@(Unipol dic) =
    in foldr
         (\a b -> (a |* one) + (b * u))
         (IM.findWithDefault zero n dic |* one)
-        [IM.findWithDefault zero k dic | k <- [0 .. n -1]]
+        [IM.findWithDefault zero k dic | k <- [0 .. n - 1]]
 {-# INLINE substWithUnipol #-}
 
 -- | The list of coefficients, in ascending order.
@@ -441,7 +440,7 @@ coeffList :: Monoidal k => Unipol k -> [k]
 coeffList (Unipol dic) =
   F.toList $
     IM.unionWith (+) dic $
-      IM.fromList [(n, zero) | n <- [0 .. maybe (- 1) (fst . fst) (IM.maxViewWithKey dic)]]
+      IM.fromList [(n, zero) | n <- [0 .. maybe (-1) (fst . fst) (IM.maxViewWithKey dic)]]
 
 {- | @'cutoff m f@ gives the polynomial \(f\) but with terms
    degree strictly less than \(m\); i.e. \(\sum_{0 \leq i < m} a_i X^i\) for
@@ -453,3 +452,8 @@ cutoff n = C.coerce (fst . IM.split (fromIntegral n) :: IM.IntMap k -> IM.IntMap
 termsUnipol ::
   Unipol k -> IM.IntMap k
 termsUnipol = C.coerce
+
+-- | Checks if all the term is non-zero. Utility function for testing purpose.
+isNormalForm :: DecidableZero k => Unipol k -> Bool
+{-# INLINE isNormalForm #-}
+isNormalForm = all (not . isZero) . runUnipol
diff --git a/halg-polynomials/test/Algebra/Algorithms/GroebnerSpec.hs b/halg-polynomials/test/Algebra/Algorithms/GroebnerSpec.hs
new file mode 100644
index 00000000..93f19682
--- /dev/null
+++ b/halg-polynomials/test/Algebra/Algorithms/GroebnerSpec.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+module Algebra.Algorithms.GroebnerSpec where
+
+import Algebra.Algorithms.Groebner
+import Algebra.Internal (KnownNat, SNat, pattern Nil, pattern (:<))
+import Algebra.Prelude.Core hiding ((===))
+import Algebra.Ring.Ideal
+import Algebra.Ring.Polynomial
+import Control.Monad
+import qualified Data.Foldable as F
+import Data.List (delete, tails)
+import qualified Data.Sized as SV
+import Numeric.Field.Fraction (Fraction)
+import Test.Tasty
+import Test.Tasty.ExpectedFailure (expectFail, ignoreTestBecause)
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+import Utils
+
+asGenListOf :: Gen [a] -> a -> Gen [a]
+asGenListOf = const
+
+type Microsecs = Int
+
+minutes, seconds :: Int -> Microsecs
+seconds n = n * 1000000
+minutes n = n * seconds 60
+
+test_divModPolynomial :: TestTree
+test_divModPolynomial =
+  testGroup
+    "divModPolynomial"
+    [ testProperty "remainder cannot be diveided by any denoms (ternary)" $
+        withMaxSuccess 10 $
+          setSize 10 $
+            within (minutes 5) $ checkForTypeNat [1 .. 4] checkindivisible
+    , testProperty "satisfies a_i f_i /= 0 ==> deg(f) >= deg (a_i f_i)" $
+        withMaxSuccess 10 $
+          setSize 10 $
+            within (minutes 5) $ checkForTypeNat [1 .. 4] checkdegdecay
+    , testProperty "divides correctly" $
+        withMaxSuccess 10 $
+          setSize 10 $
+            within (minutes 5) $ checkForTypeNat [1 .. 4] checkdivCorrect
+    ]
+
+-- spec :: Spec
+test_modPolynomial :: TestTree
+test_modPolynomial =
+  testGroup
+    "modPolynomial"
+    [ testProperty "Generates the same remainder as divModPolynomial" $
+        setSize 10 $
+          withMaxSuccess 10 $
+            within (minutes 5) $
+              checkForTypeNat [1 .. 4] $ \(sdim :: SNat n) ->
+                forAll (ratPolynomialOfArity sdim) $ \poly ->
+                  forAll (idealOfArity sdim) $ \ideal ->
+                    let gs = F.toList ideal
+                     in (poly `modPolynomial` gs) === snd (divModPolynomial poly gs)
+    ]
+
+test_calcGroebnerBasis :: TestTree
+test_calcGroebnerBasis =
+  testGroup "calcGroebnerBasis" $
+    [ testProperty "passes S-test" $
+        setSize 3 $
+          withMaxSuccess 10 $
+            within (minutes 5) $ checkForTypeNat [2 .. 3] checkpassesSTest
+    , testProperty "passes S-test (regression)" $
+        once $
+          conjoin
+            [ counterexample (show i) $ passesSTest i
+            | SomeIdeal i <- gbRegress
+            ]
+    , testProperty "divides all original generators" $
+        withMaxSuccess 10 $
+          setSize 5 $
+            within (minutes 5) $ checkForTypeNat [2 .. 3] checkgroebnerDivsOrig
+    , expectFail $
+        testCase "generates the same ideal as original" $
+          assertFailure "need example"
+    , testProperty "produces minimal basis" $
+        withMaxSuccess 10 $
+          setSize 5 $
+            within (minutes 5) $ checkForTypeNat [2 .. 3] checkisMinimal
+    , testProperty "produces reduced basis" $
+        withMaxSuccess 10 $
+          setSize 5 $
+            within (minutes 5) $ checkForTypeNat [2 .. 3] checkisReduced
+    ]
+
+test_isIdealMember :: TestTree
+test_isIdealMember =
+  testGroup
+    "isIdealMember"
+    [ expectFail $
+        testCase "determins membership correctly" $
+          assertFailure "not implemented"
+    ]
+
+test_intersection :: TestTree
+test_intersection =
+  testGroup
+    "intersection"
+    [ testProperty "can calculate correctly" $
+        setSize 4 $
+          withMaxSuccess 25 $
+            within (minutes 5) $ checkForTypeNat [2 .. 3] checkintersection
+    , testCase "can solve test-cases correctly" $
+        forM_ icsBinary $ \(IC i j ans) ->
+          F.toList (intersection [toIdeal i, toIdeal j]) @?= ans
+    ]
+
+checkintersection :: KnownNat n => SNat n -> Property
+checkintersection sdim =
+  forAll (idealOfArity sdim) $ \ideal ->
+    forAll (idealOfArity sdim) $ \jdeal ->
+      forAll (ratPolynomialOfArity sdim) $ \f ->
+        (f `isIdealMember` ideal && f `isIdealMember` jdeal)
+          == f `isIdealMember` intersection [ideal, jdeal]
+
+checkisMinimal :: KnownNat n => SNat n -> Property
+checkisMinimal sdim =
+  forAll (idealOfArity sdim) $ \ideal ->
+    let gs = calcGroebnerBasis ideal
+     in all ((== 1) . leadingCoeff) gs
+          && all (\f -> all (\g -> not $ leadingMonomial g `divs` leadingMonomial f) (delete f gs)) gs
+
+checkisReduced :: KnownNat n => SNat n -> Property
+checkisReduced sdim =
+  forAll (idealOfArity sdim) $ \ideal ->
+    let gs = calcGroebnerBasis ideal
+     in all ((== 1) . leadingCoeff) gs
+          && all (\f -> all (\g -> all (\(_, m) -> not $ leadingMonomial g `divs` m) $ getTerms f) (delete f gs)) gs
+
+checkpassesSTest :: KnownNat n => SNat n -> Property
+checkpassesSTest sdim =
+  forAll (sized $ \size -> vectorOf size (ratPolynomialOfArity sdim)) passesSTest
+
+passesSTest :: (Field (Coefficient poly), IsOrderedPolynomial poly) => [poly] -> Bool
+passesSTest ideal =
+  let gs = calcGroebnerBasis $ toIdeal ideal
+   in all (isZero . (`modPolynomial` gs)) [sPolynomial f g | (f : fs) <- init $ tails gs, g <- fs]
+
+checkgroebnerDivsOrig :: KnownNat n => SNat n -> Property
+checkgroebnerDivsOrig sdim =
+  forAll (elements [3 .. 15]) $ \count ->
+    forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
+      let gs = calcGroebnerBasis $ toIdeal ideal
+       in all ((== 0) . (`modPolynomial` gs)) ideal
+
+checkdivCorrect :: KnownNat n => SNat n -> Property
+checkdivCorrect sdim =
+  forAll (ratPolynomialOfArity sdim) $ \poly ->
+    forAll (idealOfArity sdim) $ \ideal ->
+      let dvs = generators ideal
+          (qds, r) = poly `divModPolynomial` dvs
+       in poly == sum (map (uncurry (*)) qds) + r
+
+checkindivisible :: KnownNat n => SNat n -> Property
+checkindivisible sdim =
+  forAll (ratPolynomialOfArity sdim) $ \poly ->
+    forAll (idealOfArity sdim) $ \ideal ->
+      let dvs = generators ideal
+          (_, r) = changeOrder Grevlex poly `divModPolynomial` dvs
+       in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r) dvs
+
+checkdegdecay :: KnownNat n => SNat n -> Property
+checkdegdecay sdim =
+  forAll (ratPolynomialOfArity sdim) $ \poly ->
+    forAll (idealOfArity sdim) $ \ideal ->
+      let dvs = generators ideal
+          (qs, _) = poly `divModPolynomial` dvs
+       in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
+
+data IntersectCase r ord n = IC [OrderedPolynomial r ord n] [OrderedPolynomial r ord n] [OrderedPolynomial r ord n]
+
+icsBinary :: [IntersectCase (Fraction Integer) Grevlex 2]
+icsBinary =
+  let [x, y] = F.toList allVars
+   in [IC [x * y] [y] [x * y]]
+
+data SomeIdeal where
+  SomeIdeal :: (Show poly, Field (Coefficient poly), IsOrderedPolynomial poly) => [poly] -> SomeIdeal
+
+gbRegress :: [SomeIdeal]
+gbRegress =
+  [ let [x, y, z] = vars
+     in SomeIdeal @(OrderedPolynomial Rational Grevlex 3)
+          [ x * y ^ 3 * z ^ 4
+          , (1 % 3) * x ^ 3 * y ^ 4 * z ^ 2 + 3 * x * y ^ 2 * z ^ 4
+          , -x ^ 3 * y ^ 3 * z ^ 3 + x ^ 4 * y * z ^ 4
+          ]
+  ]
diff --git a/halg-polynomials/test/Algebra/Ring/Polynomial/ListSpec.hs b/halg-polynomials/test/Algebra/Ring/Polynomial/ListSpec.hs
new file mode 100644
index 00000000..2dfae5b6
--- /dev/null
+++ b/halg-polynomials/test/Algebra/Ring/Polynomial/ListSpec.hs
@@ -0,0 +1,177 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -Wno-type-defaults #-}
+
+module Algebra.Ring.Polynomial.ListSpec where
+
+import Algebra.Field.Prime
+import Algebra.Prelude.Core hiding ((===))
+import Algebra.Ring.Euclidean.Quotient (Quotient)
+import Algebra.Ring.Euclidean.Quotient.Test ()
+import Algebra.Ring.Polynomial.List
+import Test.QuickCheck
+import Test.Tasty
+import Test.Tasty.QuickCheck
+import Utils
+
+test_algebra :: TestTree
+test_algebra =
+  testGroup
+    "algebraic operations"
+    [ testGroup
+        "(+)"
+        [ testProperty "satisfies identity law (Q)" $
+            checkForTypeNat [1 .. 3] $ commutes @Rational (+)
+        , testProperty "satisfies identity law (F 5)" $
+            checkForTypeNat [1 .. 3] $ commutes @(F 5) (+)
+        , testProperty "commutes (Q)" $
+            checkForTypeNat [1 .. 3] $ identity @Rational zero (+)
+        , testProperty "commutes (F 5)" $
+            checkForTypeNat [1 .. 3] $ identity @(F 5) zero (+)
+        , testProperty "coincides with OrderedPolynomial (Q)" $
+            checkForTypeNat [1 .. 3] $ coincidesWithPolyBin @Rational (+)
+        , testProperty "coincides with OrderedPolynomial (F 5)" $
+            checkForTypeNat [1 .. 3] $ coincidesWithPolyBin @(F 5) (+)
+        ]
+    , testGroup
+        "(*)"
+        [ testProperty "satisfies identity law (Q)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ commutes @Rational (*)
+        , testProperty "satisfies identity law (F 5)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ commutes @(F 5) (*)
+        , testProperty "commutes (Q)" $
+            checkForTypeNat [1 .. 3] $ identity @Rational one (*)
+        , testProperty "commutes (F 5)" $
+            checkForTypeNat [1 .. 3] $ identity @(F 5) one (*)
+        , testProperty "coincides with OrderedPolynomial (Q)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ coincidesWithPolyBin @Rational (*)
+        , testProperty "coincides with OrderedPolynomial (F 5)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ coincidesWithPolyBin @(F 5) (*)
+        , testProperty "left distributes over + (Q)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ \case
+                (sdim :: SNat n) -> withKnownNat sdim $
+                  property $ \f g h ->
+                    let fgh = f * (g + h) :: ListPoly Rational Grevlex n
+                        fgfh = f * g + f * h
+                     in fgh === fgfh
+        , testProperty "right distributes over + (Q)" $
+            setSize 50 $
+              checkForTypeNat [1 .. 3] $ \case
+                (sdim :: SNat n) -> withKnownNat sdim $
+                  property $ \f g h ->
+                    let fgh = (f + g) * h :: ListPoly Rational Grevlex n
+                        fhgh = f * h + g * h
+                     in fgh === fhgh
+        ]
+    ]
+
+coincidesWithPolyBin ::
+  forall r n.
+  (CoeffRing r, PrettyCoeff r, Arbitrary r) =>
+  ( forall a.
+    (IsOrderedPolynomial a, Coefficient a ~ r, Arity a ~ n) =>
+    a ->
+    a ->
+    a
+  ) ->
+  SNat n ->
+  Property
+coincidesWithPolyBin bin sdim = withKnownNat sdim $
+  property $ \f g ->
+    let fgPol = bin f g :: Polynomial r n
+        fgList = bin (fromPoly f) (fromPoly g)
+     in fgList === fromPoly fgPol
+
+fromPoly ::
+  (CoeffRing r, KnownNat n, IsMonomialOrder n ord) =>
+  OrderedPolynomial r ord n ->
+  ListPoly r ord n
+fromPoly = polynomial . terms
+
+commutes ::
+  forall r n.
+  (CoeffRing r, PrettyCoeff r, Arbitrary r) =>
+  (ListPoly r Grevlex n -> ListPoly r Grevlex n -> ListPoly r Grevlex n) ->
+  SNat n ->
+  Property
+commutes op (sdim :: SNat n) = withKnownNat sdim $
+  forAll (join (liftA2 (,)) arbitrary) $ \(f, g) ->
+    op f g === op g f
+
+identity ::
+  forall r n.
+  (CoeffRing r, PrettyCoeff r, Arbitrary r) =>
+  ListPoly r Grevlex n ->
+  (ListPoly r Grevlex n -> ListPoly r Grevlex n -> ListPoly r Grevlex n) ->
+  SNat n ->
+  Property
+identity eps op (sdim :: SNat n) = withKnownNat sdim $
+  forAll arbitrary $ \f ->
+    op eps f === f .&&. op f eps === f
+
+test_normalForm :: TestTree
+test_normalForm =
+  testGroup
+    "normal form"
+    [ testProperty "addition gives normal form (F 5)" $
+        checkForTypeNat [1 .. 3] $ checkBinNF @(F 5) (+)
+    , testProperty "addition gives normal form (Q)" $
+        checkForTypeNat [1 .. 3] $ checkBinNF @Rational (+)
+    , testProperty "subtraction gives normal form (F 5)" $
+        checkForTypeNat [1 .. 3] $ checkBinNF @(F 5) (-)
+    , testProperty "subtraction gives normal form (Q)" $
+        checkForTypeNat [1 .. 3] $ checkBinNF @Rational (-)
+    , testProperty "f - f is normal form (F 5)" $
+        checkForTypeNat [1 .. 3] $ checkUnNF @(F 5) (join (-))
+    , testProperty "f - f is normal form (Q)" $
+        checkForTypeNat [1 .. 3] $ checkUnNF @Rational (join (-))
+    , testProperty "f + f + f + f + f is normal form (F 5)" $
+        checkForTypeNat [1 .. 3] $ checkUnNF @(F 5) (\f -> f + f + f + f + f)
+    , testProperty "2 f * 3 g is normal form over Z/6Z" $
+        checkForTypeNat [1 .. 3] $
+          checkBinNF @(Quotient 6 Integer)
+            ( \f g ->
+                ((fromInteger' 2 :: Quotient 6 Integer) .*. f)
+                  * ((fromInteger' 3 :: Quotient 6 Integer) .*. g)
+            )
+    , testProperty "multiplication gives normal form (F 5)" $
+        setSize 50 $
+          checkForTypeNat [1 .. 3] $ checkBinNF @(F 5) (*)
+    , testProperty "multiplication gives normal form (Q)" $
+        setSize 50 $
+          checkForTypeNat [1 .. 3] $ checkBinNF @Rational (*)
+    , testProperty "splitLeadingTerm gives normal form (F 5)" $
+        checkForTypeNat [1 .. 3] $ checkUnNF @(F 5) (snd . splitLeadingTerm)
+    ]
+
+checkUnNF ::
+  forall r n.
+  (CoeffRing r, PrettyCoeff r, Arbitrary r) =>
+  (ListPoly r Grevlex n -> ListPoly r Grevlex n) ->
+  SNat n ->
+  Property
+checkUnNF op sdim =
+  withKnownNat sdim $
+    forAll arbitrary $ \f ->
+      isNormalForm (op f)
+
+checkBinNF ::
+  forall r n.
+  (CoeffRing r, PrettyCoeff r, Arbitrary r) =>
+  (ListPoly r Grevlex n -> ListPoly r Grevlex n -> ListPoly r Grevlex n) ->
+  SNat n ->
+  Property
+checkBinNF op sdim = withKnownNat sdim $
+  forAll arbitrary $ \f g ->
+    isNormalForm (op f g)
diff --git a/halg-polynomials/test/Algebra/Ring/Polynomial/QuotientSpec.hs b/halg-polynomials/test/Algebra/Ring/Polynomial/QuotientSpec.hs
new file mode 100644
index 00000000..674e3a8c
--- /dev/null
+++ b/halg-polynomials/test/Algebra/Ring/Polynomial/QuotientSpec.hs
@@ -0,0 +1 @@
+module Algebra.Ring.Polynomial.QuotientSpec where
diff --git a/halg-polynomials/test/Algebra/Ring/Polynomial/UnivariateSpec.hs b/halg-polynomials/test/Algebra/Ring/Polynomial/UnivariateSpec.hs
new file mode 100644
index 00000000..fc67a6c1
--- /dev/null
+++ b/halg-polynomials/test/Algebra/Ring/Polynomial/UnivariateSpec.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -Wno-type-defaults #-}
+
+module Algebra.Ring.Polynomial.UnivariateSpec where
+
+import Algebra.Field.Prime
+import Algebra.Prelude.Core hiding ((===))
+import Algebra.Ring.Euclidean.Quotient (Quotient)
+import Algebra.Ring.Polynomial.Univariate
+import Test.QuickCheck
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+import Utils
+
+asGenListOf :: Gen [a] -> a -> Gen [a]
+asGenListOf = const
+
+toOP :: Unipol Integer -> OrderedPolynomial Integer Grevlex 1
+toOP = injectVars
+
+liftMult :: Unipol Integer -> Unipol Integer -> Unipol Integer
+liftMult f g =
+  let (f', g') = (toOP f, toOP g)
+   in injectVars (f' * g')
+
+test_naiveMult :: TestTree
+test_naiveMult =
+  testGroup
+    "naiveMult"
+    [ testProperty "Works as expected" $
+        setSize 5 $
+          withMaxSuccess 10 $ \f g ->
+            (f `naiveMult` g) == (f `liftMult` g)
+    ]
+
+test_karatsuba :: TestTree
+test_karatsuba =
+  testGroup
+    "karatsuba"
+    [ testProperty "Works as expected" $ \f g ->
+        setSize 5 $
+          withMaxSuccess 25 $
+            karatsuba f g == (f `liftMult` g)
+    ]
+
+test_divModUnipolByMult :: TestTree
+test_divModUnipolByMult =
+  testGroup
+    "divModUnipolByMult"
+    [ testProperty "remainder has degree smaller than divisor" $
+        setSize 5 $
+          withMaxSuccess 25 $ \f g ->
+            let (_, r) = divModUnipolByMult f (g :: Unipol (F 5))
+             in (totalDegree' f > 0 && totalDegree' g > 0)
+                  ==> totalDegree' r < totalDegree' g
+    , testProperty "divides correctly" $
+        setSize 5 $
+          withMaxSuccess 25 $ \f g ->
+            let (q, r) = divModUnipolByMult f (g :: Unipol (F 5))
+             in not (isZero g) ==> q * g + r === f
+    , testCase "passes regression tests" $
+        mapM_
+          (\((a, b), (c, d)) -> divModUnipolByMult a b @?= (c, d))
+          divModUnipolCases
+    ]
+
+test_divModUnipol :: TestTree
+test_divModUnipol =
+  testGroup
+    "divModUnipol"
+    [ testProperty "remainder has degree smaller than divisor" $
+        setSize 5 $
+          withMaxSuccess 25 $ \f g ->
+            let (_, r) = divModUnipol f (g :: Unipol (F 5))
+             in totalDegree' f > 0 && totalDegree' g > 0
+                  ==> totalDegree' r < totalDegree' g
+    , testProperty "divides correctly" $
+        setSize 5 $
+          withMaxSuccess 25 $ \f g ->
+            let (q, r) = divModUnipol f (g :: Unipol (F 5))
+             in not (isZero g)
+                  ==> q * g + r == f
+    ]
+
+test_operations :: TestTree
+test_operations =
+  testGroup
+    "Normal forms"
+    [ testProperty "addition preserves normal form (F_17)" $ \f g ->
+        isNormalForm (f + g :: Unipol (F 17))
+    , testProperty "addition preserves normal form (Q)" $ \f g ->
+        isNormalForm (f + g :: Unipol Rational)
+    , testProperty "subtraction preserves normal form (Q)" $ \f g ->
+        isNormalForm (f - g :: Unipol Rational)
+    , testProperty "subtraction preserves normal form (F_17)" $ \f g ->
+        isNormalForm (f - g :: Unipol (F 17))
+    , testProperty "f - f is normal form (F_17)" $ \f ->
+        isNormalForm (f - f :: Unipol (F 17))
+    , testProperty "f - f is normal form (Q)" $ \f ->
+        isNormalForm (f - f :: Unipol Rational)
+    , testProperty "division preserves normal form (Q)" $
+        withMaxSuccess 25 $
+          \(NonZero f) (NonZero g) ->
+            let [f', g'] = sortOn (Down . leadingMonomial) [f, g :: Unipol Rational]
+                (q, r) = f' `divModUnipol` g'
+             in isNormalForm q .&&. isNormalForm r
+    , testProperty "division preserves normal form (F_17)" $ \(NonZero f) (NonZero g) ->
+        let [f', g'] = sortOn (Down . leadingMonomial) [f, g :: Unipol (F 17)]
+            (q, r) = f' `divModUnipol` g'
+         in isNormalForm q .&&. isNormalForm r
+    , testProperty "splitLeadingTerm preserves normal form (Q)" $ \f ->
+        let (_, g) = splitLeadingTerm (f :: Unipol Rational)
+         in isNormalForm g
+    , testProperty "multiplication preserves normal form (F_5)" $
+        setSize 10 $
+          withMaxSuccess 25 $ \f g ->
+            tabulate "# of terms" (map (show . length . terms) [f, g]) $
+              isNormalForm (f * g :: Unipol (F 5))
+    , testProperty "f + f + f + f + f = 0 and it's normal form (F_5)" $ \f ->
+        let f5 = f + f + f + f + f :: Unipol (F 5)
+         in f5 === 0 .&&. isNormalForm f5
+    , testCase "2 x * 3x^2 = 0 and normal form (in Z/6Z)" $ do
+        let mustBeZero = (2 * #x) * (3 * #x ^ 2) :: Unipol (Quotient 6 Integer)
+        mustBeZero @?= 0
+        assertBool "not normal form!" $ isNormalForm mustBeZero
+    ]
+
+divModUnipolCases :: [((Unipol (F 5), Unipol (F 5)), (Unipol (F 5), Unipol (F 5)))]
+divModUnipolCases =
+  [((3 * x ^ 57 + x ^ 56 + x ^ 55 + 2 * x ^ 52 + 2 * x ^ 51 + 4 * x ^ 50 + x ^ 49 + 4 * x ^ 48 + 3 * x ^ 47 + 4 * x ^ 46 + 3 * x ^ 45 + 3 * x ^ 44 + 3 * x ^ 42 + 3 * x ^ 41 + x ^ 40 + x ^ 39 + 2 * x ^ 38 + 3 * x ^ 37 + x ^ 36 + 2 * x ^ 35 + 4 * x ^ 34 + 3 * x ^ 33 + 4 * x ^ 32 + 3 * x ^ 31 + x ^ 30 + 3 * x ^ 28 + x ^ 26 + x ^ 25 + 3 * x ^ 24 + x ^ 22 + 4 * x ^ 21 + 3 * x ^ 20 + 2 * x ^ 19 + 4 * x ^ 18 + 4 * x ^ 17 + 2 * x ^ 16 + x ^ 15 + 3 * x ^ 13 + 2 * x ^ 12 + x ^ 11 + x ^ 10 + 4 * x ^ 9 + 4 * x ^ 8 + 2 * x ^ 7 + x ^ 6 + 2 * x ^ 5 + 4 * x ^ 4 + 2 * x ^ 3 + 2 * x ^ 2 + 3 * x + 4, 3 * x ^ 19 + 2 * x ^ 18 + 4 * x ^ 17 + 3 * x ^ 16 + 4 * x ^ 13 + 3 * x ^ 12 + x ^ 11 + 4 * x ^ 10 + 2 * x ^ 8 + 2 * x ^ 7 + 2 * x ^ 6 + 4 * x ^ 4 + 2 * x ^ 3 + 4 * x ^ 2 + 3 * x + 2), (x ^ 38 + 3 * x ^ 37 + 2 * x ^ 36 + 2 * x ^ 35 + 3 * x ^ 34 + 4 * x ^ 33 + 4 * x ^ 32 + 2 * x ^ 31 + 2 * x ^ 30 + 3 * x ^ 29 + 2 * x ^ 28 + 3 * x ^ 26 + x ^ 25 + x ^ 24 + 3 * x ^ 23 + 2 * x ^ 22 + 2 * x ^ 20 + 3 * x ^ 18 + 2 * x ^ 17 + 3 * x ^ 16 + 4 * x ^ 15 + x ^ 14 + 4 * x ^ 13 + 3 * x ^ 12 + 2 * x ^ 11 + 3 * x ^ 10 + 2 * x ^ 9 + 4 * x ^ 7 + 3 * x ^ 5 + 2 * x ^ 4 + 3 * x ^ 3 + 2 * x ^ 2 + x + 2, 2 * x ^ 18 + 4 * x ^ 17 + 3 * x ^ 16 + 2 * x ^ 15 + 4 * x ^ 14 + 4 * x ^ 12 + 2 * x ^ 11 + 4 * x ^ 10 + 3 * x ^ 8 + x ^ 6 + 3 * x ^ 4 + 2 * x ^ 3 + 2 * x ^ 2))]
+  where
+    x = var 0
diff --git a/halg-polynomials/test/Algebra/Ring/PolynomialSpec.hs b/halg-polynomials/test/Algebra/Ring/PolynomialSpec.hs
new file mode 100644
index 00000000..b2effcf4
--- /dev/null
+++ b/halg-polynomials/test/Algebra/Ring/PolynomialSpec.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+module Algebra.Ring.PolynomialSpec where
+
+import Algebra.Algorithms.Groebner
+import Algebra.Internal
+import Algebra.Ring.Ideal
+import Algebra.Ring.Polynomial
+import qualified Data.Matrix as M
+import qualified Data.Vector as V
+import Test.QuickCheck
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+import Utils
+
+asGenListOf :: Gen [a] -> a -> Gen [a]
+asGenListOf = const
+
+prop_passesSTest :: Property
+prop_passesSTest = forAll (elements [1 .. 5]) $ \n ->
+  case toSomeSNat n of
+    (SomeSNat (sdim :: SNat n)) -> withKnownNat sdim $
+      forAll (elements [3 .. 15]) $ \count ->
+        forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
+          let gs = calcGroebnerBasis $ toIdeal ideal
+           in all ((== 0) . (`modPolynomial` gs)) [sPolynomial f g | f <- gs, g <- gs, f /= g]
+
+prop_groebnerDivsOrig :: Property
+prop_groebnerDivsOrig = forAll (elements [1 .. 5]) $ \n -> case toSomeSNat n of
+  SomeSNat (sdim :: SNat n) ->
+    withKnownNat sdim $
+      forAll (elements [3 .. 15]) $ \count ->
+        forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
+          let gs = calcGroebnerBasis $ toIdeal ideal
+           in all ((== 0) . (`modPolynomial` gs)) ideal
+
+prop_divCorrect :: Property
+prop_divCorrect = forAll (elements [1 .. 5]) $ \n -> case toSomeSNat n of
+  SomeSNat (sdim :: SNat n) ->
+    withKnownNat sdim $
+      forAll (ratPolynomialOfArity sdim) $ \poly ->
+        forAll (idealOfArity sdim) $ \ideal ->
+          let dvs = generators ideal
+              (qds, r) = poly `divModPolynomial` dvs
+           in poly == sum (map (uncurry (*)) qds) + r
+
+prop_indivisible :: Property
+prop_indivisible = forAll (elements [1 .. 5]) $ \n -> case toSomeSNat n of
+  SomeSNat (sdim :: SNat n) ->
+    withKnownNat sdim $
+      forAll (ratPolynomialOfArity sdim) $ \poly ->
+        forAll (idealOfArity sdim) $ \ideal ->
+          let dvs = generators ideal
+              (_, r) = changeOrder Grevlex poly `divModPolynomial` dvs
+           in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r) dvs
+
+prop_degdecay :: Property
+prop_degdecay = forAll (elements [1 .. 5]) $ \n -> case toSomeSNat n of
+  SomeSNat (sdim :: SNat n) ->
+    withKnownNat sdim $
+      forAll (ratPolynomialOfArity sdim) $ \poly ->
+        forAll (idealOfArity sdim) $ \ideal ->
+          let dvs = generators ideal
+              (qs, _) = poly `divModPolynomial` dvs
+           in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
+
+rank :: (Ord r, Fractional r) => M.Matrix r -> Int
+rank mat =
+  let Just (u, _, _, _, _, _) = M.luDecomp' mat
+   in V.foldr (\a acc -> if a /= 0 then acc + 1 else acc) (0 :: Int) $ M.getDiag u
diff --git a/halg-polynomials/test/GroebnerSpec.hs b/halg-polynomials/test/GroebnerSpec.hs
deleted file mode 100644
index a60a8158..00000000
--- a/halg-polynomials/test/GroebnerSpec.hs
+++ /dev/null
@@ -1,154 +0,0 @@
-{-# LANGUAGE DataKinds, ExplicitNamespaces, GADTs, NoImplicitPrelude #-}
-{-# LANGUAGE PatternSynonyms, ScopedTypeVariables, TypeApplications  #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-module GroebnerSpec where
-import Algebra.Algorithms.Groebner
-import Algebra.Internal            (pattern (:<), KnownNat, pattern Nil, SNat)
-import Algebra.Prelude.Core        hiding ((===))
-import Algebra.Ring.Ideal
-import Algebra.Ring.Polynomial
-import Utils
-
-import           Control.Monad
-import qualified Data.Foldable            as F
-import           Data.List                (delete, tails)
-import qualified Data.Sized       as SV
-import           Numeric.Field.Fraction   (Fraction)
-import           Test.Hspec
-import           Test.Hspec.QuickCheck
-import           Test.QuickCheck
-import           Test.QuickCheck.Property
-
-asGenListOf :: Gen [a] -> a -> Gen [a]
-asGenListOf = const
-
-type Microsecs = Int
-minutes, seconds :: Int -> Microsecs
-seconds n = n * 1000000
-minutes n = n * seconds 60
-
-setSize :: Testable prop => Int -> prop -> Property
-setSize n p =  MkProperty (sized ((`resize` unProperty (property p)) . const n))
-
-spec :: Spec
-spec = parallel $ do
-  describe "divModPolynomial" $ modifyMaxSize (const 10) $ modifyMaxSuccess (const 10) $ do
-    prop "remainder cannot be diveided by any denoms (ternary)" $
-      within (minutes 5) $ checkForTypeNat [1..4] prop_indivisible
-    prop "satisfies a_i f_i /= 0 ==> deg(f) >= deg (a_i f_i)" $
-      within (minutes 5) $ checkForTypeNat [1..4] prop_degdecay
-    prop "divides correctly" $
-      within (minutes 5) $ checkForTypeNat [1..4] prop_divCorrect
-  describe "modPolynomial" $ modifyMaxSize (const 10) $ modifyMaxSuccess (const 10) $
-    prop "Generates the same remainder as divModPolynomial" $
-      within (minutes 5) $ checkForTypeNat [1..4] $ \(sdim :: SNat n) ->
-      forAll (ratPolynomialOfArity sdim) $ \poly ->
-      forAll (idealOfArity sdim) $ \ideal ->
-        let gs = F.toList ideal
-        in (poly `modPolynomial` gs) === snd (divModPolynomial poly gs)
-  describe "calcGroebnerBasis" $ modifyMaxSize (const 5) $ modifyMaxSuccess (const 10) $ do
-    prop "passes S-test" $
-      setSize 3 $
-      within (minutes 5) $ checkForTypeNat [2..3] prop_passesSTest
-    prop "passes S-test (regression)" $ once $
-      conjoin [ counterexample (show i) $ passesSTest i
-              | SomeIdeal i <- gbRegress
-              ]
-    prop "divides all original generators" $
-      within (minutes 5) $ checkForTypeNat [2..3] prop_groebnerDivsOrig
-    it "generates the same ideal as original" $
-      pendingWith "need example"
-    it "produces minimal basis" $
-      within (minutes 5) $ checkForTypeNat [2..3] prop_isMinimal
-    it "produces reduced basis" $
-      within (minutes 5) $ checkForTypeNat [2..3] prop_isReduced
-  describe "isIdealMember" $
-    it "determins membership correctly" $
-    pendingWith "need example"
-  describe "intersection" $ modifyMaxSize (const 4) $ modifyMaxSuccess (const 25) $ do
-    it "can calculate correctly" $
-      within (minutes 5) $ checkForTypeNat [2..3] prop_intersection
-    it "can solve test-cases correctly" $
-      forM_ ics_binary $ \(IC i j ans) ->
-      F.toList (intersection [toIdeal i, toIdeal j]) `shouldBe` ans
-
-prop_intersection :: KnownNat n => SNat n -> Property
-prop_intersection sdim =
-  forAll (idealOfArity sdim) $ \ideal ->
-  forAll (idealOfArity sdim) $ \jdeal ->
-  forAll (ratPolynomialOfArity sdim) $ \f ->
-  (f `isIdealMember` ideal && f `isIdealMember` jdeal)
-  == f `isIdealMember` intersection [ideal, jdeal]
-
-prop_isMinimal :: KnownNat n => SNat n -> Property
-prop_isMinimal sdim =
-  forAll (idealOfArity sdim) $ \ideal ->
-  let gs = calcGroebnerBasis ideal
-  in all ((== 1) . leadingCoeff) gs &&
-     all (\f -> all (\g -> not $ leadingMonomial g `divs` leadingMonomial f) (delete f gs)) gs
-
-prop_isReduced :: KnownNat n => SNat n -> Property
-prop_isReduced sdim =
-  forAll (idealOfArity sdim) $ \ideal ->
-  let gs = calcGroebnerBasis ideal
-  in all ((== 1) . leadingCoeff) gs &&
-     all (\f -> all (\g -> all (\(_, m) -> not $ leadingMonomial g `divs` m) $ getTerms f) (delete f gs)) gs
-
-prop_passesSTest :: KnownNat n => SNat n -> Property
-prop_passesSTest sdim =
-  forAll (sized $ \size -> vectorOf size (ratPolynomialOfArity sdim)) passesSTest
-
-passesSTest :: (Field (Coefficient poly), IsOrderedPolynomial poly) => [poly] -> Bool
-passesSTest ideal =
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all (isZero . (`modPolynomial` gs)) [sPolynomial f g | (f : fs) <- init $ tails gs, g <- fs]
-
-prop_groebnerDivsOrig :: KnownNat n => SNat n -> Property
-prop_groebnerDivsOrig sdim =
-  forAll (elements [3..15]) $ \count ->
-  forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all ((== 0) . (`modPolynomial` gs)) ideal
-
-prop_divCorrect :: KnownNat n => SNat n -> Property
-prop_divCorrect sdim =
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qds, r) = poly `divModPolynomial` dvs
-  in poly == sum (map (uncurry (*)) qds) + r
-
-prop_indivisible :: KnownNat n => SNat n -> Property
-prop_indivisible sdim =
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (_, r) = changeOrder Grevlex poly `divModPolynomial` dvs
-  in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r)  dvs
-
-prop_degdecay :: KnownNat n => SNat n -> Property
-prop_degdecay sdim =
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qs, _) = poly `divModPolynomial` dvs
-  in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
-
-data IntersectCase r ord n = IC [OrderedPolynomial r ord n] [OrderedPolynomial r ord n] [OrderedPolynomial r ord n]
-
-ics_binary :: [IntersectCase (Fraction Integer) Grevlex 2]
-ics_binary =
-  let [x, y] = F.toList allVars
-  in [IC [x*y] [y] [x*y]]
-
-data SomeIdeal where
-  SomeIdeal :: (Show poly, Field (Coefficient poly), IsOrderedPolynomial poly) => [poly] -> SomeIdeal
-
-gbRegress :: [SomeIdeal]
-gbRegress =
-  [ let [x,y,z] = vars
-    in SomeIdeal @(OrderedPolynomial Rational Grevlex 3)
-       [ x * y ^3* z ^4
-       , (1 % 3) * x ^3* y ^4* z ^2 + 3* x * y ^2* z ^4
-       , - x ^3* y ^3* z ^3 +  x ^4* y * z ^4]
-  ]
diff --git a/halg-polynomials/test/PolynomialSpec.hs b/halg-polynomials/test/PolynomialSpec.hs
deleted file mode 100644
index 36669cc8..00000000
--- a/halg-polynomials/test/PolynomialSpec.hs
+++ /dev/null
@@ -1,68 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-module PolynomialSpec where
-import Algebra.Algorithms.Groebner
-import Algebra.Internal
-import Algebra.Ring.Ideal
-import Algebra.Ring.Polynomial
-import Utils
-
-import qualified Data.Matrix           as M
-import qualified Data.Vector           as V
-import           Test.Hspec
-import           Test.Hspec.QuickCheck
-import           Test.QuickCheck
-
-asGenListOf :: Gen [a] -> a -> Gen [a]
-asGenListOf = const
-
-spec :: Spec
-spec = parallel $ do
-  return ()
-
-prop_passesSTest :: SNat n -> Property
-prop_passesSTest sdim = withKnownNat sdim $
-  forAll (elements [3..15]) $ \count ->
-  forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all ((== 0) . (`modPolynomial` gs)) [sPolynomial f g | f <- gs, g <- gs, f /= g]
-
-prop_groebnerDivsOrig :: SNat n -> Property
-prop_groebnerDivsOrig sdim =
-  withKnownNat sdim $
-  forAll (elements [3..15]) $ \count ->
-  forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all ((== 0) . (`modPolynomial` gs)) ideal
-
-prop_divCorrect :: SNat n -> Property
-prop_divCorrect sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qds, r) = poly `divModPolynomial` dvs
-  in poly == sum (map (uncurry (*)) qds) + r
-
-prop_indivisible :: SNat n -> Property
-prop_indivisible sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (_, r) = changeOrder Grevlex poly `divModPolynomial` dvs
-  in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r)  dvs
-
-prop_degdecay :: SNat n -> Property
-prop_degdecay sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qs, _) = poly `divModPolynomial` dvs
-  in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
-
-rank :: (Ord r, Fractional r) => M.Matrix r -> Int
-rank mat =
-  let Just (u, _, _, _,_, _) = M.luDecomp' mat
-  in V.foldr (\a acc -> if a /= 0 then acc + 1 else acc) (0 :: Int) $ M.getDiag u
diff --git a/halg-polynomials/test/QuotientSpec.hs b/halg-polynomials/test/QuotientSpec.hs
deleted file mode 100644
index 53374262..00000000
--- a/halg-polynomials/test/QuotientSpec.hs
+++ /dev/null
@@ -1,71 +0,0 @@
-{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeApplications #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-module QuotientSpec where
-import Algebra.Algorithms.Groebner
-import Algebra.Internal
-import Algebra.Prelude.Core             (Fraction)
-import Algebra.Ring.Ideal
-import Algebra.Ring.Polynomial
-import Algebra.Ring.Polynomial.Quotient
-import Utils
-
-import qualified Data.Matrix           as M
-import qualified Data.Vector           as V
-import           Test.Hspec
-import           Test.Hspec.QuickCheck
-import           Test.QuickCheck
-
-asGenListOf :: Gen [a] -> a -> Gen [a]
-asGenListOf = const
-
-spec :: Spec
-spec = parallel $ do
-  return ()
-
-prop_passesSTest :: SNat n -> Property
-prop_passesSTest sdim =
-  withKnownNat sdim $
-  forAll (elements [3..15]) $ \count ->
-  forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all ((== 0) . (`modPolynomial` gs)) [sPolynomial f g | f <- gs, g <- gs, f /= g]
-
-prop_groebnerDivsOrig :: SNat n -> Property
-prop_groebnerDivsOrig sdim =
-  withKnownNat sdim $
-  forAll (elements [3..15]) $ \count ->
-  forAll (vectorOf count (ratPolynomialOfArity sdim)) $ \ideal ->
-  let gs = calcGroebnerBasis $ toIdeal ideal
-  in all ((== 0) . (`modPolynomial` gs)) ideal
-
-prop_divCorrect :: SNat n -> Property
-prop_divCorrect sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qds, r) = poly `divModPolynomial` dvs
-  in poly == sum (map (uncurry (*)) qds) + r
-
-prop_indivisible :: SNat n -> Property
-prop_indivisible sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (_, r) = changeOrder Grevlex poly `divModPolynomial` dvs
-  in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r)  dvs
-
-prop_degdecay :: forall n. SNat n -> Property
-prop_degdecay sdim =
-  withKnownNat sdim $
-  forAll (ratPolynomialOfArity sdim) $ \poly ->
-  forAll (idealOfArity sdim) $ \ideal ->
-  let dvs = generators ideal
-      (qs, _) = (poly :: Polynomial (Fraction Integer) n) `divModPolynomial` dvs
-  in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
-
-rank :: (Ord r, Fractional r) => M.Matrix r -> Int
-rank mat =
-  let Just (u, _, _, _,_, _) = M.luDecomp' mat
-  in V.foldr (\a acc -> if a /= 0 then acc + 1 else acc) (0 :: Int) $ M.getDiag u
diff --git a/halg-polynomials/test/Spec.hs b/halg-polynomials/test/Spec.hs
index a824f8c3..3b9b2477 100644
--- a/halg-polynomials/test/Spec.hs
+++ b/halg-polynomials/test/Spec.hs
@@ -1 +1 @@
-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+{-# OPTIONS_GHC -F -pgmF tasty-discover  -optF --tree-display #-}
diff --git a/halg-polynomials/test/UnivariateSpec.hs b/halg-polynomials/test/UnivariateSpec.hs
deleted file mode 100644
index a4c12b4b..00000000
--- a/halg-polynomials/test/UnivariateSpec.hs
+++ /dev/null
@@ -1,65 +0,0 @@
-{-# LANGUAGE DataKinds, ExplicitNamespaces, GADTs, PatternSynonyms #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports -Wno-type-defaults #-}
-module UnivariateSpec where
-import           Algebra.Algorithms.Groebner
-import           Algebra.Field.Prime
-import           Algebra.Internal                   (pattern (:<), KnownNat,
-                                                     pattern Nil, SNat)
-import           Algebra.Ring.Polynomial            (OrderedPolynomial)
-import           Algebra.Ring.Polynomial.Univariate
-import           Control.Monad
-import qualified Data.Foldable                      as F
-import           Data.List                          (delete)
-import qualified Data.Sized                 as SV
-import           Numeric.Decidable.Zero
-import           Numeric.Field.Fraction             (Fraction)
-import           Test.Hspec
-import           Test.Hspec.QuickCheck
-import           Test.QuickCheck
-import           Utils
-
-asGenListOf :: Gen [a] -> a -> Gen [a]
-asGenListOf = const
-
-toOP :: Unipol Integer -> OrderedPolynomial Integer Grevlex 1
-toOP = injectVars
-
-liftMult :: Unipol Integer -> Unipol Integer -> Unipol Integer
-liftMult f g =
-  let (f', g') = (toOP f, toOP g)
-  in injectVars (f' * g')
-
-spec :: Spec
-spec = parallel $ do
-  describe "naiveMult" $ modifyMaxSize (const 5) $ modifyMaxSuccess (const 10) $ do
-    prop "Works as expected" $ \f g ->
-      (f `naiveMult` g) == (f `liftMult` g)
-  describe "karatsuba"$ modifyMaxSize (const 5) $ modifyMaxSuccess (const 25)  $ do
-    prop "Works as expected" $ \f g ->
-      (karatsuba f g) == (f `liftMult` g)
-  describe "divModUnipolByMult" $  modifyMaxSize (const 5) $ modifyMaxSuccess (const 25)  $ do
-    prop "remainder has degree smaller than divisor" $ \f g ->
-      (totalDegree' f > 0 && totalDegree' g > 0) ==>
-      let (q, r) = divModUnipolByMult f (g :: Unipol (F 5))
-      in totalDegree' r < totalDegree' g
-    prop "divides correctly" $ \f g ->
-      not (isZero g) ==>
-      let (q, r) = divModUnipolByMult f (g :: Unipol (F 5))
-      in q * g + r == f
-    it "passes regression tests" $ do
-      mapM_ (\((a,b),(c,d)) -> divModUnipolByMult a b `shouldBe` (c, d))
-        divModUnipolCases
-  describe "divModUnipol" $  modifyMaxSize (const 5) $ modifyMaxSuccess (const 25)  $ do
-    prop "remainder has degree smaller than divisor" $ \f g ->
-      totalDegree' f > 0 && totalDegree' g > 0 ==>
-      let (q, r) = divModUnipol f (g :: Unipol (F 5))
-      in totalDegree' r < totalDegree' g
-    prop "divides correctly" $ \f g ->
-      not (isZero g) ==>
-      let (q, r) = divModUnipol f (g :: Unipol (F 5))
-      in q * g + r == f
-
-divModUnipolCases :: [((Unipol (F 5), Unipol (F 5)), (Unipol (F 5), Unipol (F 5)))]
-divModUnipolCases =
-  [((3*x^57 + x^56 + x^55 + 2*x^52 + 2*x^51 + 4*x^50 + x^49 + 4*x^48 + 3*x^47 + 4*x^46 + 3*x^45 + 3*x^44 + 3*x^42 + 3*x^41 + x^40 + x^39 + 2*x^38 + 3*x^37 + x^36 + 2*x^35 + 4*x^34 + 3*x^33 + 4*x^32 + 3*x^31 + x^30 + 3*x^28 + x^26 + x^25 + 3*x^24 + x^22 + 4*x^21 + 3*x^20 + 2*x^19 + 4*x^18 + 4*x^17 + 2*x^16 + x^15 + 3*x^13 + 2*x^12 + x^11 + x^10 + 4*x^9 + 4*x^8 + 2*x^7 + x^6 + 2*x^5 + 4*x^4 + 2*x^3 + 2*x^2 + 3*x + 4, 3*x^19 +2*x^18 +4*x^17 +3*x^16 +4*x^13 +3*x^12 + x^11 +4*x^10 +2*x^8 +2*x^7 +2*x^6 +4*x^4 +2*x^3 +4*x^2 +3*x + 2),(x^38 +3*x^37 +2*x^36 +2*x^35 +3*x^34 +4*x^33 +4*x^32 +2*x^31 +2*x^30 +3*x^29 +2*x^28 +3*x^26 + x^25 + x^24 +3*x^23 +2*x^22 +2*x^20 +3*x^18 +2*x^17 +3*x^16 +4*x^15 + x^14 +4*x^13 +3*x^12 +2*x^11 +3*x^10 +2*x^9 +4*x^7 +3*x^5 +2*x^4 +3*x^3 +2*x^2 + x + 2,2*x^18 +4*x^17 +3*x^16 +2*x^15 +4*x^14 +4*x^12 +2*x^11 +4*x^10 +3*x^8 + x^6 +3*x^4 +2*x^3 +2*x^2))]
-  where x = var 0
diff --git a/halg-polynomials/test/Utils.hs b/halg-polynomials/test/Utils.hs
index ae9aff08..081efe7c 100644
--- a/halg-polynomials/test/Utils.hs
+++ b/halg-polynomials/test/Utils.hs
@@ -1,22 +1,39 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs                   #-}
-{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude                     #-}
-{-# LANGUAGE NoMonomorphismRestriction, ScopedTypeVariables, TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances                                         #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
+
 module Utils (module Utils, module Algebra.TestUtils) where
-import Algebra.Field.Prime
+
 import Algebra.Prelude.Core
 import Algebra.Ring.Polynomial.Univariate
+import Algebra.Ring.Polynomial.List
 import Algebra.TestUtils
-import AlgebraicPrelude                   ()
+import AlgebraicPrelude ()
 import Test.QuickCheck
 
-instance (Arbitrary k, KnownNat n, CoeffRing k, IsMonomialOrder n o)
-      => Arbitrary (OrderedPolynomial k o n) where
+instance
+  (Arbitrary k, KnownNat n, CoeffRing k, IsMonomialOrder n o) =>
+  Arbitrary (OrderedPolynomial k o n)
+  where
   arbitrary = arbitraryPolynomial
 
-instance (Arbitrary k, CoeffRing k)
-      => Arbitrary (Unipol k) where
+instance
+  (Arbitrary k, KnownNat n, CoeffRing k, IsMonomialOrder n o) =>
+  Arbitrary (ListPoly k o n)
+  where
+  arbitrary = arbitraryPolynomial
+
+instance
+  (Arbitrary k, CoeffRing k) =>
+  Arbitrary (Unipol k)
+  where
   arbitrary = arbitraryPolynomial
 
 idealOfArity :: SNat n -> Gen (Ideal (Polynomial (Fraction Integer) n))
@@ -25,6 +42,11 @@ idealOfArity sn = withKnownNat sn arbitrary
 ratPolynomialOfArity :: KnownNat n => SNat n -> Gen (Polynomial (Fraction Integer) n)
 ratPolynomialOfArity = polynomialOfArity
 
-polynomialOfArity :: (KnownNat n, DecidableZero k, Field k, Eq k, Arbitrary k)
-                  => SNat n -> Gen (Polynomial k n)
+polynomialOfArity ::
+  (KnownNat n, DecidableZero k, Field k, Eq k, Arbitrary k) =>
+  SNat n ->
+  Gen (Polynomial k n)
 polynomialOfArity sn = withKnownNat sn (runWrapPolynomial <$> arbitrary)
+
+setSize :: Testable prop => Int -> prop -> Property
+setSize = mapSize . const
diff --git a/hie.yaml b/hie.yaml
index 6b8cc707..7c510f67 100644
--- a/hie.yaml
+++ b/hie.yaml
@@ -1,6 +1,6 @@
 cradle:
   stack:
-    stackYaml: stack-8.10.7.yaml
+    stackYaml: stack-9.0.2.yaml
     components:
     - path: "halg-algebraic/src"
       component: "halg-algebraic:lib"
diff --git a/stack-9.0.1.yaml.lock b/stack-9.0.1.yaml.lock
deleted file mode 100644
index adfc332c..00000000
--- a/stack-9.0.1.yaml.lock
+++ /dev/null
@@ -1,156 +0,0 @@
-# This file was autogenerated by Stack.
-# You should not edit this file by hand.
-# For more information, please see the documentation at:
-#   https://docs.haskellstack.org/en/stable/lock_files
-
-packages:
-- completed:
-    hackage: algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129
-    pantry-tree:
-      size: 5556
-      sha256: 2dea7d23304c09c902fb1f90f45b1b22df6ded47fb717742cca119f9f3667b21
-  original:
-    hackage: algebra-4.3.1
-- completed:
-    hackage: control-monad-loop-0.1@sha256:2b8d9fbc6e53f2c8f679188952b90f2c69507d1c1efd8867beb64591a22b341c,1106
-    pantry-tree:
-      size: 466
-      sha256: e0bb7221ac929e5fe3722f4838551e962589a8fed18199d9791385864855f466
-  original:
-    hackage: control-monad-loop-0.1
-- completed:
-    hackage: ghc-typelits-presburger-0.6.0.0@sha256:2132a3ae673c41983df257ee748a2ca785566ce563f689e73c27e7e469ca366e,3192
-    pantry-tree:
-      size: 836
-      sha256: b17dbaf95553b8d64684ca21cf3f7c97df60d8b5663a7da5db07751188346f1d
-  original:
-    hackage: ghc-typelits-presburger-0.6.0.0
-- completed:
-    hackage: singletons-presburger-0.6.0.0@sha256:40a5cea2b54499f417fdbe5750ebf8c5d73098c93862a580937ab1614a1eec96,2655
-    pantry-tree:
-      size: 313
-      sha256: d24aeaf800d5ac50d258a4ab093bbfec63d80b9f00c97a318b53dc41eb0871c7
-  original:
-    hackage: singletons-presburger-0.6.0.0
-- completed:
-    hackage: equational-reasoning-0.7.0.0@sha256:f7fe162978543f8c3ccaf338dbdef7d69537c3aa87f062225d9e5d3585698c7e,1952
-    pantry-tree:
-      size: 496
-      sha256: 96e180f8d67b22588b00bc29c84d7534ffdc958406921789a7e78a4eb263263b
-  original:
-    hackage: equational-reasoning-0.7.0.0@rev:2
-- completed:
-    hackage: sized-1.0.0.0@sha256:7f0dbfcf0eab2861b5661b8c4a7f04c4a7f6d9b64dd8e9eef1e27ddbdc6c638f,1770
-    pantry-tree:
-      size: 517
-      sha256: f80506533e6e89c261853170245b148e2fc23cde9d6408d457c7418121f72f62
-  original:
-    hackage: sized-1.0.0.0
-- completed:
-    hackage: type-natural-1.1.0.0@sha256:94c2d827a4dc0a27fae61e94378f0c23460dda0683a42414b851a912f7d0a203,2730
-    pantry-tree:
-      size: 1401
-      sha256: cfcf4ca82d7c26578816b7e3095500a4ff774a594dea748378d70a92973c792b
-  original:
-    hackage: type-natural-1.1.0.0
-- completed:
-    hackage: repa-3.4.1.4@sha256:5a99bde69fe96a18d70aae23f47c8f719b1134558dca3ee5a7c15423b68a132e,3323
-    pantry-tree:
-      size: 2965
-      sha256: 060bec03e51bb6f40acc52c70f8e36804e18f80590b09dc8141352f1b14b03e7
-  original:
-    hackage: repa-3.4.1.4@rev:8
-- completed:
-    hackage: profunctors-5.6.2@sha256:4db306297d827cf65a32d9124d6f1a23105479ebb1988783006578bc5d4209da,2377
-    pantry-tree:
-      size: 1588
-      sha256: 5e640a3a4613c8850d19d322b4ec8444345deb0cf4ee020590da82e2d657be26
-  original:
-    hackage: profunctors-5.6.2
-- completed:
-    hackage: unamb-0.2.7@sha256:ce5db0575bca8ca04c9e9dce3ba75b6f9e5ceea834c6ba4fae45aca6fa963334,2385
-    pantry-tree:
-      size: 217
-      sha256: c3c4ac7408c2999b6779714459d2433ff2495f90161d7c3ca349ca3aa6386be8
-  original:
-    hackage: unamb-0.2.7
-- completed:
-    hackage: singletons-th-3.0@sha256:111458cb40a11d2c9e31bfb384d17a52fcac55c17b4c3519944a38511ae7d834,4605
-    pantry-tree:
-      size: 2538
-      sha256: 5473c540967821a7eaa7eb8b405873443cec00fffc4dc7598cfc553ddb2f21bd
-  original:
-    hackage: singletons-th-3.0
-- completed:
-    hackage: th-desugar-1.12@sha256:019a2b121ed5de5f8a6af40ee7754511708566fe86def9533e3a54ec074be20e,3764
-    pantry-tree:
-      size: 1675
-      sha256: 9a6788ef0f02fb8dc76c7673f201dc3452f73df0fba7ff2197a49e7c5c5df879
-  original:
-    hackage: th-desugar-1.12
-- completed:
-    hackage: singletons-3.0@sha256:e20fe9cd8825812641171c71a5eec566dce9efdab24d21d53a738ce9e7de9472,2901
-    pantry-tree:
-      size: 713
-      sha256: 86243c5d1bf78f8261dee4cfd32a04b3503115ba2491685083b417a6cb10bb73
-  original:
-    hackage: singletons-3.0
-- completed:
-    hackage: singletons-base-3.0@sha256:a6fad461d9b500b0df4dbcfca0a0185b5f09fe13c546a57acbcad70a0357f20a,6915
-    pantry-tree:
-      size: 23714
-      sha256: c63aad30407b78f46c2ce035e35be0ac858e952f82a70783d44cc19fdfa41f45
-  original:
-    hackage: singletons-base-3.0
-- completed:
-    hackage: generic-deriving-1.14@sha256:c9c6782a3cdce2f2bcaf891e0ffbf06df871e68498574b73a565771dc084273c,6835
-    pantry-tree:
-      size: 2248
-      sha256: 2e75303f186f68c1a5d7ebaa62df33ee326bedbf746ed363a64607578118341d
-  original:
-    hackage: generic-deriving-1.14
-- completed:
-    hackage: th-expand-syns-0.4.8.0@sha256:cf548f09dbe38d1e4649d9713a64b7d192c3bfb1c47894fa3538ed5503858fc0,1796
-    pantry-tree:
-      size: 550
-      sha256: 899e5bed5f4a537d19a589529fd9cfcb2dac4aa1a7eaed64df7acdc8261a2172
-  original:
-    hackage: th-expand-syns-0.4.8.0
-- completed:
-    hackage: syb-0.7.2.1@sha256:bf42655a213402215299e435c52f799e76cbec0b984cd7153d6b9af8a1c0803f,3815
-    pantry-tree:
-      size: 3396
-      sha256: 3ee55cc33d69da2953e7093f99199fbc0bfa9d90dccd19cac101d09befa5bbb3
-  original:
-    hackage: syb-0.7.2.1
-- completed:
-    hackage: indexed-traversable-instances-0.1@sha256:3aaf97040001bbe583e29c2b9c7d41660df265e6565a0d2ac09a3ed5b8bc21be,2874
-    pantry-tree:
-      size: 427
-      sha256: d69630ba4b548b72eed15553586ce7b1e574cd8e4cc5b30d506ab3a697b26502
-  original:
-    hackage: indexed-traversable-instances-0.1
-- completed:
-    hackage: lens-5.0.1@sha256:c97fbe43ae6fe21d73f1a023d776bb05cd492f0afd1b3c3ff43e246af91f6852,15544
-    pantry-tree:
-      size: 8291
-      sha256: 915f23967904b51276fbeb1181eb51b3d958f48273bb10de3914bea8184c0336
-  original:
-    hackage: lens-5.0.1
-- completed:
-    size: 201218
-    url: https://github.com/Bodigrim/arithmoi/archive/29099a51cfddb3c77f726e86a5784553456e10ab.tar.gz
-    name: arithmoi
-    version: 0.11.0.1
-    sha256: 3632e71c810c33721d3521b0d868dacaabccf326274b8d9e026c50ce21219fae
-    pantry-tree:
-      size: 10365
-      sha256: bfc8cba90cf593574bd3f1bdd9d3163e921e342f2e83d0ba9d61f75900574d96
-  original:
-    url: https://github.com/Bodigrim/arithmoi/archive/29099a51cfddb3c77f726e86a5784553456e10ab.tar.gz
-snapshots:
-- completed:
-    size: 567669
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/12.yaml
-    sha256: facf6cac73b22a83ca955b580a98a7a09ed71f8f974c7a55d28e608c23e689a9
-  original: lts-17.12
diff --git a/stack-9.0.2.yaml.lock b/stack-9.0.2.yaml.lock
new file mode 100644
index 00000000..70cfd523
--- /dev/null
+++ b/stack-9.0.2.yaml.lock
@@ -0,0 +1,26 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages:
+- completed:
+    hackage: control-monad-loop-0.1@sha256:2b8d9fbc6e53f2c8f679188952b90f2c69507d1c1efd8867beb64591a22b341c,1106
+    pantry-tree:
+      size: 466
+      sha256: e0bb7221ac929e5fe3722f4838551e962589a8fed18199d9791385864855f466
+  original:
+    hackage: control-monad-loop-0.1
+- completed:
+    hackage: unamb-0.2.7@sha256:ce5db0575bca8ca04c9e9dce3ba75b6f9e5ceea834c6ba4fae45aca6fa963334,2385
+    pantry-tree:
+      size: 217
+      sha256: c3c4ac7408c2999b6779714459d2433ff2495f90161d7c3ca349ca3aa6386be8
+  original:
+    hackage: unamb-0.2.7
+snapshots:
+- completed:
+    size: 616897
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/0.yaml
+    sha256: bbf2be02f17940bac1f87cb462d4fb0c3355de6dcfc53d84f4f9ad3ee2164f65
+  original: lts-19.0
diff --git a/stack.yaml b/stack.yaml
index 62d4418e..242ae1ce 120000
--- a/stack.yaml
+++ b/stack.yaml
@@ -1 +1 @@
-stack-8.10.7.yaml
\ No newline at end of file
+stack-9.0.2.yaml
\ No newline at end of file
diff --git a/stack.yaml.lock b/stack.yaml.lock
index 51f32581..70cfd523 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -4,13 +4,6 @@
 #   https://docs.haskellstack.org/en/stable/lock_files
 
 packages:
-- completed:
-    hackage: algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129
-    pantry-tree:
-      size: 5556
-      sha256: 2dea7d23304c09c902fb1f90f45b1b22df6ded47fb717742cca119f9f3667b21
-  original:
-    hackage: algebra-4.3.1
 - completed:
     hackage: control-monad-loop-0.1@sha256:2b8d9fbc6e53f2c8f679188952b90f2c69507d1c1efd8867beb64591a22b341c,1106
     pantry-tree:
@@ -27,7 +20,7 @@ packages:
     hackage: unamb-0.2.7
 snapshots:
 - completed:
-    size: 586110
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/21.yaml
-    sha256: ce4fb8d44f3c6c6032060a02e0ebb1bd29937c9a70101c1517b92a87d9515160
-  original: lts-18.21
+    size: 616897
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/0.yaml
+    sha256: bbf2be02f17940bac1f87cb462d4fb0c3355de6dcfc53d84f4f9ad3ee2164f65
+  original: lts-19.0