diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,4 @@
+Copyright (c) 2013 Henning Thielemann
 Copyright (c) 2008 Peter Gavin
 All rights reserved.
 
diff --git a/Test.hs b/Test.hs
--- a/Test.hs
+++ b/Test.hs
@@ -220,6 +220,15 @@
 testMax3 :: Max D6 D1 -> D6
 testMax3 = Prelude.id
 
+testLog1 :: Log2Ceil D8 -> D3
+testLog1 = Prelude.id
+testLog2 :: Log2Ceil D9 -> D4
+testLog2 = Prelude.id
+testLog3 :: Log2Ceil D2 -> D1
+testLog3 = Prelude.id
+testLog4 :: Log2Ceil D1 -> D0
+testLog4 = Prelude.id
+
 class TestIter n zero where
     testIter :: n -> zero -> Prelude.String
 
diff --git a/Types/Data/Num.hs b/Types/Data/Num.hs
--- a/Types/Data/Num.hs
+++ b/Types/Data/Num.hs
@@ -20,6 +20,7 @@
     , reifyIntegralD
     , reifyPositiveD
     , reifyNegativeD
+    , reifyNaturalD
 #endif
     ) where
 
@@ -47,4 +48,8 @@
 reifyNegativeD :: Integer -> (forall s. (NegativeT s, Repr s ~ Decimal) => s -> a) -> Maybe a
 #endif
 reifyNegativeD = reifyNegative decimal
+#if __GLASGOW_HASKELL__ >= 704
+reifyNaturalD :: Integer -> (forall s. (NaturalT s, Repr s ~ Decimal) => s -> a) -> Maybe a
+#endif
+reifyNaturalD = reifyNatural decimal
 #endif
diff --git a/Types/Data/Num/Decimal/Ops.hs b/Types/Data/Num/Decimal/Ops.hs
--- a/Types/Data/Num/Decimal/Ops.hs
+++ b/Types/Data/Num/Decimal/Ops.hs
@@ -135,6 +135,13 @@
 type instance IsNegative' DecN       = False
 type instance IsNegative' (xh :. xl) = False
 
+-- type family IsNatural x
+type instance IsNatural (Dec x) = IsNatural' x
+type family IsNatural' x
+type instance IsNatural' (Neg' x)   = False
+type instance IsNatural' DecN       = True
+type instance IsNatural' (xh :. xl) = True
+
 -- type family Neg x
 type instance Neg (Dec DecN)     = Dec DecN
 type instance Neg (Dec (Neg' x)) = Dec x
@@ -761,6 +768,15 @@
 type instance Pow2' (Neg' x)   y = DecN
 type instance Pow2' DecN       y = y
 type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)
+
+---------------
+-- Logarithm
+type instance Log2Ceil (Dec x) = Dec (Log2C' (Pred' x) DecN)
+
+type family Log2C' x y
+type instance Log2C' (Neg' x) y   = DecN
+type instance Log2C' DecN     y   = y
+type instance Log2C' (xh :. xl) y = Log2C' (Div2' (xh :. xl)) (Succ' y)
 
 ---------------
 -- Compare
diff --git a/Types/Data/Num/Ops.hs b/Types/Data/Num/Ops.hs
--- a/Types/Data/Num/Ops.hs
+++ b/Types/Data/Num/Ops.hs
@@ -22,6 +22,8 @@
     , isZeroT
     , IsNegative
     , isNegativeT
+    , IsNatural
+    , isNaturalT
     , Succ
     , succT
     , Pred
@@ -40,6 +42,8 @@
     , mul2T
     , Pow2
     , pow2T
+    , Log2Ceil
+    , log2CeilT
     , DivMod
     , divModT
     , Div
@@ -57,6 +61,7 @@
     , NegativeT
     , reifyPositive
     , reifyNegative
+    , reifyNatural
     ) where
 
 import Types.Data.Bool
@@ -82,6 +87,10 @@
 isNegativeT :: x -> IsNegative x
 isNegativeT _ = undefined
 
+type family IsNatural x
+isNaturalT :: x -> IsNatural x
+isNaturalT _ = undefined
+
 type family Succ x
 succT :: x -> Succ x
 succT _ = undefined
@@ -139,9 +148,12 @@
 pow2T :: x -> Pow2 x
 pow2T _ = undefined
 
-class IntegerT x => NaturalT x
-instance (IntegerT x, IsNegative x ~ False) => NaturalT x
+type family Log2Ceil x
+log2CeilT :: x -> Log2Ceil x
+log2CeilT _ = undefined
 
+class IntegerT x => NaturalT x
+instance (IntegerT x, IsNatural x  ~ True) => NaturalT x
 class IntegerT x => PositiveT x
 instance (IntegerT x, IsPositive x ~ True) => PositiveT x
 class IntegerT x => NegativeT x
@@ -158,6 +170,7 @@
 --- positive and negative assertions: unsafe, in a trusted kernel
 data AssertPos x
 data AssertNeg x
+data AssertNat x
 
 assertPos :: x -> AssertPos x
 assertPos _ = undefined
@@ -165,9 +178,20 @@
 assertNeg :: x -> AssertNeg x
 assertNeg _ = undefined
 
+assertNat :: x -> AssertNat x
+assertNat _ = undefined
+
 type instance IsPositive (AssertPos x) = True
+type instance IsPositive (AssertNeg x) = False
+
+type instance IsNegative (AssertPos x) = False
 type instance IsNegative (AssertNeg x) = True
+type instance IsNegative (AssertNat x) = False
 
+type instance IsNatural  (AssertPos x) = True
+type instance IsNatural  (AssertNeg x) = False
+type instance IsNatural  (AssertNat x) = True
+
 instance IntegerT x => IntegerT (AssertPos x) where 
     fromIntegerT _ = fromIntegerT (undefined :: x)
     type Repr (AssertPos x) = Repr x
@@ -176,10 +200,17 @@
     fromIntegerT _ = fromIntegerT (undefined :: x)
     type Repr (AssertNeg x) = Repr x
 
+instance IntegerT x => IntegerT (AssertNat x) where
+    fromIntegerT _ = fromIntegerT (undefined :: x)
+    type Repr (AssertNat x) = Repr x
+
 reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a
 reifyPositive r n k | n > 0     = Just (reifyIntegral r n (k . assertPos))
                     | otherwise = Nothing
 
 reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a
 reifyNegative r n k | n < 0     = Just (reifyIntegral r n (k . assertNeg))
+                    | otherwise = Nothing
+reifyNatural :: IntegerR r => r -> Integer -> (forall s. (NaturalT s, Repr s ~ r) => s -> a) -> Maybe a
+reifyNatural r n k | n >= 0     = Just (reifyIntegral r n (k . assertNat))
                     | otherwise = Nothing
diff --git a/Types/Data/Ord.hs b/Types/Data/Ord.hs
--- a/Types/Data/Ord.hs
+++ b/Types/Data/Ord.hs
@@ -26,14 +26,19 @@
     , isGTT
     , (:<:)
     , ltT
+    , LTT
     , (:<=:)
     , leT
+    , LET
     , (:==:)
     , eqT
+    , EQT
     , (:>=:)
     , geT
+    , GET
     , (:>:)
     , gtT
+    , GTT
     , Min
     , minT
     , Max
@@ -86,31 +91,43 @@
 type instance x :<: y = IsLT (Compare x y)
 ltT :: x -> y -> x :<: y
 ltT _ _ = Prelude.undefined
+class LTT x y
+instance ((x :<: y) ~ True) => LTT x y
 
 type family x :<=: y
 type instance x :<=: y = Not (x :>: y)
 leT :: x -> y -> x :<=: y
 leT _ _ = Prelude.undefined
+class LET x y
+instance ((x :<=: y) ~ True) => LET x y
 
 type family x :==: y
 type instance x :==: y = IsEQ (Compare x y)
 eqT :: x -> y -> x :==: y
 eqT _ _ = Prelude.undefined
+class EQT x y
+instance ((x :==: y) ~ True) => EQT x y
 
 type family x :/=: y
 type instance x :/=: y = Not (x :==: y)
 neT :: x -> y -> x :/=: y
 neT _ _ = Prelude.undefined
+class NET x y
+instance ((x :/=: y) ~ True) => NET x y
 
 type family x :>=: y
 type instance x :>=: y = Not (x :<: y)
 geT :: x -> y -> x :>=: y
 geT _ _ = Prelude.undefined
+class GET x y
+instance ((x :>=: y) ~ True) => GET x y
 
 type family x :>: y
 type instance x :>: y = IsGT (Compare x y)
 gtT :: x -> y -> x :>: y
 gtT _ _ = Prelude.undefined
+class GTT x y
+instance ((x :>: y) ~ True) => GTT x y
 
 type family Min x y
 type instance Min x y = If (x :<=: y) x y
diff --git a/tfp.cabal b/tfp.cabal
--- a/tfp.cabal
+++ b/tfp.cabal
@@ -1,27 +1,35 @@
 name:           tfp
-version:        0.6
-cabal-version:  >= 1.6
+version:        0.7
 build-type:     Simple
 license:        BSD3
 license-file:   LICENSE
-copyright:      Copyright (c) 2008 Peter Gavin
-author:         Peter Gavin
-maintainer:     pgavin@gmail.com
-homepage:       http://github.com/pgavin/tfp
+copyright:      Copyright (c) 2013 Henning Thielemann, 2008 Peter Gavin
+author:         Peter Gavin, Henning Thielemann
+maintainer:     haskell@henning-thielemann.de
+homepage:       http://www.haskell.org/haskellwiki/Type_arithmetic
 stability:      alpha
-package-url:    http://github.com/pgavin/tfp
-synopsis:       Type-level programming library using type families
-description:	TFP (short for Type Family Programming) provides implementations of type-level integers and booleans,
-		and (eventually) simple type-level data structures. It uses type families as functions to produce new types,
-		which provides an intuitive way to parameterize data types and functions on numerical values at compile time.
-category:       Data
-tested-with:    GHC == 6.9.0
+synopsis:       Type-level integers, booleans, lists using type families
+description:
+  TFP is an abbreviation for Type Family Programming.
+  It provides implementations of type-level integers and booleans,
+  and (eventually) simple type-level data structures.
+  It uses type families as functions to produce new types,
+  which provides an intuitive way to parameterize data types
+  and functions on numerical values at compile time.
+category:       Type System
+tested-with:    GHC == 7.4.2
+cabal-version:  >= 1.6
 
-source-repository head {
-  type:         git
-  location:     git@github.com:pgavin/tfp.git
-}
+source-repository head
+  type:         darcs
+  location:     http://code.haskell.org/~thielema/tfp/
 
+source-repository this
+  tag:          0.7
+  type:         darcs
+  location:     http://code.haskell.org/~thielema/tfp/
+
+
 flag build-test
   description: Build the tfp-test test program
   default: False
@@ -34,18 +42,18 @@
                   Rank2Types, FlexibleContexts
   build-depends:  base >= 3.0 && < 5, template-haskell >= 2.0
   exposed-modules:
-    Data.SizedInt,
-    Data.SizedWord,
-    Types,
-    Types.Base,
-    Types.Data.Bool,
+    Data.SizedInt
+    Data.SizedWord
+    Types
+    Types.Base
+    Types.Data.Bool
     Types.Data.Num
     Types.Data.Num.Ops
-    Types.Data.Num.Decimal,
+    Types.Data.Num.Decimal
     Types.Data.Num.Decimal.Literals
     Types.Data.Num.Decimal.Literals.TH
     Types.Data.Num.Decimal.Digits
-    Types.Data.List,
+    Types.Data.List
     Types.Data.Ord
   other-modules:
     Types.Data.Num.Decimal.Ops