diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2012-2014, Iago Abal
+Copyright (c) 2012-2016, Iago Abal
 
 All rights reserved.
 
diff --git a/bv.cabal b/bv.cabal
--- a/bv.cabal
+++ b/bv.cabal
@@ -1,15 +1,15 @@
 
 Name:                bv
-Version:             0.3.0
+Version:             0.4.0
 Synopsis:            Bit-vector arithmetic library
-Description:         Bit-vectors implemented as a wrapper over integers.
+Description:         Bit-vectors implemented as a thin wrapper over integers.
 Homepage:            http://bitbucket.org/iago/bv-haskell
 Bug-reports:         http://bitbucket.org/iago/bv-haskell/issues
 License:             BSD3
 License-file:        LICENSE
 Author:              Iago Abal <mail@iagoabal.eu>
 Maintainer:          Iago Abal <mail@iagoabal.eu>
-Copyright:           2012-2014 Iago Abal
+Copyright:           2012-2016 Iago Abal
 Category:            Data, Bit Vectors
 Build-type:          Simple
 Cabal-version:       >=1.6
@@ -18,8 +18,12 @@
   type:     mercurial
   location: https://bitbucket.org/iago/bv-haskell
 
+Flag gmp
+     Description: Using Integer GMP backend.
+     Default: True
+
 Flag test
-     Description: Build the test suite, including an executable to run it.
+     Description: Build the test suite, and an executable to run it.
      Default: False
      Manual: True
 
@@ -27,10 +31,12 @@
   Exposed-modules:     Data.BitVector
   -- Other-modules:
   Hs-Source-Dirs:      src
-  ghc-options:         -Wall
+  ghc-options:         -Wall -O2
   Extensions:          CPP
-  Other-Extensions:    BangPatterns, DeriveDataTypeable
+  Other-Extensions:    BangPatterns, DeriveDataTypeable, MagicHash
   Build-depends:       base >=4.6 && <5
+  if impl(ghc) && flag(gmp)
+    Build-depends: integer-gmp, ghc-prim
 
 Executable bv-tester
   if flag(test)
@@ -46,5 +52,5 @@
   Hs-Source-Dirs:      src, test
   ghc-options:         -Wall
   Extensions:          CPP
-  Other-Extensions:    BangPatterns, DeriveDataTypeable
+  Other-Extensions:    BangPatterns, DeriveDataTypeable, MagicHash
 
diff --git a/src/Data/BitVector.hs b/src/Data/BitVector.hs
--- a/src/Data/BitVector.hs
+++ b/src/Data/BitVector.hs
@@ -3,9 +3,13 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 
+#if MIN_VERSION_integer_gmp(0,5,1)
+{-# LANGUAGE MagicHash #-}
+#endif
+
 -- |
 -- Module    : Data.BitVector
--- Copyright : (c) 2012-2014 Iago Abal
+-- Copyright : (c) 2012-2016 Iago Abal
 --             (c) 2012-2013 HASLab & University of Minho
 -- License   : BSD3
 -- Maintainer: Iago Abal <mail@iagoabal.eu>
@@ -31,7 +35,9 @@
   , size, width
   , nat, uint, int
     -- * Creation
+  , nil
   , bitVec
+  , bitVecs
   , ones, zeros
     -- * Test
   , isNat
@@ -43,15 +49,17 @@
     -- * Indexing
   , (@.), index
   , (@@), extract
+  , (@:)
   , (!.)
   , least, most
   , msb, lsb, msb1, lsb1
   -- * Arithmetic
   , signumI
+  , pow
   , sdiv, srem, smod
   , lg2
   -- * List-like operations
-  , (#), cat
+  , (#), cat, append, concat
   , zeroExtend, signExtend
   , foldl, foldl_
   , foldr, foldr_
@@ -76,9 +84,6 @@
   , showBin
   , showOct
   , showHex
-  -- * Utilities
-  , maxNat
-  , integerWidth
   ) where
 
 import           Control.Exception ( assert )
@@ -88,19 +93,21 @@
 import qualified Data.Bool as Bool
 import           Data.Data ( Data )
 import qualified Data.List as List
-  ( foldr, foldl1'
-  , length
-  , map
-  , maximum
-  )
+import           Data.Monoid ( Monoid(..) )
 import           Data.Ord
 import           Data.Typeable ( Typeable )
 
+#if MIN_VERSION_integer_gmp(0,5,1)
+import qualified GHC.Integer.Logarithms as I
+import           GHC.Prim ( (+#) )
+import           GHC.Types ( Int(..) )
+#endif
+
 import           Prelude
   ( Char
   , Eq(..)
   , Enum(..), Num(..)
-  , Integral(..), Int, Integer
+  , Integral(..), Integer
   , Maybe(..)
   , Real(..)
   , Show(..), String
@@ -114,6 +121,7 @@
   )
 
 {-# DEPRECATED foldl_, foldr_, reverse_, replicate_, and_, or_, group_, not_ "Use corresponding versions without underscore" #-}
+{-# DEPRECATED cat "Use (#) or append instead" #-}
 
 ----------------------------------------------------------------------
 --- Bit-vectors
@@ -157,6 +165,11 @@
 ----------------------------------------------------------------------
 --- Construction
 
+-- | The /empty/ bit-vector, ie. @[0]0@.
+nil :: BV
+nil = BV 0 0
+{-# INLINE nil #-}
+
 -- | Create a bit-vector given a size and an integer value.
 --
 -- >>> bitVec 4 3
@@ -168,10 +181,28 @@
 -- [4]15
 bitVec :: Integral a => Int -> a -> BV
 bitVec n a | n < 0     = error "Data.BitVector.bitVec: negative size"
-           | a >= 0    = BV n $ fromIntegral a
-           | otherwise = negate $ BV n $ fromIntegral (-a)
+           | a >= 0    = BV n (a' `mod` 2^n)
+           | otherwise = negate $ BV n ((-a') `mod` 2^n)
+  where a' = fromIntegral a
 {-# INLINE bitVec #-}
 
+-- | List of bit-vector literals of the same size
+--
+-- When a list of integer literals is interpreted as a list of bit-vectors,
+-- 'fromInteger' is applied to each element invidually:
+--
+-- >>> [1,3,5] :: [BV]
+-- [ [1]1, [2]3, [3]5 ]
+--
+-- Sometimes we want to specify a list of bit-vectors literals of the same
+-- size, and for that we can use 'bitVects':
+--
+-- >>> bitVecs 3 [1,3,5]
+-- [ [3]1, [3]3, [3]5 ]
+bitVecs :: Integral a => Int -> [a] -> [BV]
+bitVecs = List.map . bitVec
+{-# INLINE bitVecs #-}
+
 -- | Create a mask of ones.
 ones :: Int -> BV
 ones n | n < 0     = error "Data.BitVector.ones: negative size"
@@ -205,9 +236,11 @@
 
 instance Eq BV where
   (BV _ a) == (BV _ b) = a == b
+  {-# INLINE (==) #-}
 
 instance Ord BV where
   compare = comparing nat
+  {-# INLINE compare #-}
 
 -- | Fixed-size equality.
 --
@@ -273,7 +306,7 @@
 ----------------------------------------------------------------------
 --- Indexing
 
-infixl 9 @., @@, !.
+infixl 9 @., @@, @:, !.
 
 -- | Bit indexing.
 --
@@ -313,6 +346,20 @@
 extract j i = (@@ (j,i))
 {-# INLINE extract #-}
 
+-- | Bit list indexing.
+--
+-- prop> u @: is ==. fromBits $ List.map (u @.) is
+(@:) :: Integral ix => BV -> [ix] -> BV
+(BV n a) @: is = fromBits $ List.map testBitAux is
+  -- NB: Failing _late_ (the bounds check is done by 'testBitAux') avoids
+  -- duplicating calls to 'fromIntegral' **and** this code should allow GHC
+  -- to fuse 'fodlr' (from inlining 'frombits') with 'map'.
+  where testBitAux i
+          | i' >= 0 && i' < n = testBit a i'
+          | otherwise = error "Data.BitVector.(@:): index out of bounds"
+          where i' = fromIntegral i
+{-# INLINE (@:) #-}
+
 -- | Reverse bit-indexing.
 --
 -- Index starting from the most significant bit.
@@ -396,13 +443,26 @@
 instance Num BV where
   (BV n1 a) + (BV n2 b) = BV n $ (a + b) `mod` 2^n
     where n = max n1 n2
+  {-# INLINE (+) #-}
+  {-# INLINE (-) #-}
   (BV n1 a) * (BV n2 b) = BV n $ (a * b) `mod` 2^n
     where n = max n1 n2
-  negate (BV n a) = BV n $ 2^n - a
+  {-# INLINE (*) #-}
+  negate u@(BV _ 0) = u
+  negate   (BV n a) = BV n $ 2^n - a
+  {-# INLINE negate #-}
   abs u | msb u     = negate u
         | otherwise = u
+  {-# INLINE abs #-}
   signum u = bitVec 2 $ signum $ int u
+  {-# INLINE signum #-}
+#if MIN_VERSION_integer_gmp(0,5,1)
+  fromInteger i = bitVec n i
+    where n = I# (I.integerLog2# i +# 1#)
+#else
   fromInteger i = bitVec (integerWidth i) i
+#endif
+  {-# INLINE fromInteger #-}
 
 -- | Bit-vector 'signum' as an 'Integral'.
 signumI :: Integral a => BV -> a
@@ -420,9 +480,23 @@
   quotRem (BV n1 a) (BV n2 b) = (BV n q,BV n r)
     where n = max n1 n2
           (q,r) = quotRem a b
+  {-# INLINE quotRem #-}
   divMod = quotRem
+  {-# INLINE divMod #-}
   toInteger = nat
+  {-# INLINE toInteger #-}
 
+-- | Bit-vector exponentiation.
+--
+-- @pow [n]k e@ computes @k@ raised to @e@ modulo @n@.
+--
+-- This is faster than Haskell's (^) operator because it performs
+-- modulo division just once. Besides, @a^0 == [1]0@ !!!
+pow :: Integral exp => BV -> exp -> BV
+pow (BV n a) e = BV n (a^e `mod` m)
+  where m = 2^n
+{-# INLINE pow #-}
+
 -- | 2's complement signed division.
 sdiv :: BV -> BV -> BV
 sdiv u@(BV n1 _) v@(BV n2 _) = bitVec n q
@@ -450,7 +524,12 @@
 lg2 :: BV -> BV
 lg2 (BV _ 0) = error "Data.BitVector.lg2: zero bit-vector"
 lg2 (BV n 1) = BV n 0
+#if MIN_VERSION_integer_gmp(0,5,1)
+lg2 (BV n a) = BV n (toInteger a')
+  where a' = I# (I.integerLog2# a)
+#else
 lg2 (BV n a) = BV n $ toInteger $ integerWidth (a-1)
+#endif
 {-# INLINE lg2 #-}
 
 ----------------------------------------------------------------------
@@ -459,13 +538,29 @@
 infixr 5 #
 
 -- | Concatenation of two bit-vectors.
-(#), cat :: BV -> BV -> BV
+(#), cat, append :: BV -> BV -> BV
 (BV n a) # (BV m b) = BV (n + m) ((a `shiftL` m) + b)
 {-# INLINE (#) #-}
 
 cat = (#)
 {-# INLINE cat #-}
 
+append = (#)
+{-# INLINE append #-}
+
+-- | An alias for 'join'.
+concat :: [BV] -> BV
+concat = join
+
+-- This is the most sensible monoid instance until we have size types!
+instance Monoid BV where
+  mempty  = nil
+  {-# INLINE mempty #-}
+  mappend = (#)
+  {-# INLINE mappend #-}
+  mconcat = join
+  {-# INLINE mconcat #-}
+
 -- | Logical extension.
 --
 -- >>> zeroExtend 3 [1]1
@@ -535,9 +630,11 @@
 
 -- | Conjunction.
 --
--- @and == foldr1 (.&.)@
+-- Essentially, @and == foldr1 (.&.)@.
+--
+-- Returns @[1]1@ if the input list is empty.
 and, and_ :: [BV] -> BV
-and [] = error "Data.BitVector.and: empty list"
+and [] = ones 1
 and ws = BV n' $ List.foldl1' (.&.) $ List.map nat ws
   where n' = List.maximum $ List.map size ws
 and_ = and
@@ -545,9 +642,11 @@
 
 -- | Disjunction.
 --
--- @or == foldr1 (.|.)@
+-- Essentially, @or == foldr1 (.|.)@.
+--
+-- Returns @[1]0@ if the input list is empty.
 or, or_ :: [BV] -> BV
-or [] = error "Data.BitVector.or: empty list"
+or [] = zeros 1
 or ws = BV n' $ List.foldl1' (.|.) $ List.map nat ws
   where n' = List.maximum $ List.map size ws
 or_ = or
@@ -588,12 +687,12 @@
                 a' = a `shiftR` n'
 {-# INLINE splitInteger #-}
 
--- | Concatenate a list of bit-vectors.
+-- | Concatenate a (possibly empty) list of bit-vectors.
 --
 -- >>> join [[2]3,[2]2]
 -- [4]14
 join :: [BV] -> BV
-join = List.foldl1' (#)
+join = List.foldl' (#) nil
 {-# INLINE join #-}
 
 ----------------------------------------------------------------------
@@ -604,17 +703,24 @@
 instance Bits BV where
   (BV n1 a) .&. (BV n2 b) = BV n $ a .&. b
     where n = max n1 n2
+  {-# INLINE (.&.) #-}
   (BV n1 a) .|. (BV n2 b) = BV n $ a .|. b
     where n = max n1 n2
+  {-# INLINE (.|.) #-}
   (BV n1 a) `xor` (BV n2 b) = BV n $ a `xor` b
     where n = max n1 n2
+  {-# INLINE xor #-}
   complement (BV n a) = BV n $ 2^n - 1 - a
+  {-# INLINE complement #-}
 #if MIN_VERSION_base(4,7,0)
   zeroBits = BV 1 0
+  {-# INLINE zeroBits #-}
 #endif
   bit i = BV (i+1) (2^i)
+  {-# INLINE bit #-}
   testBit (BV n a) i | i < n     = testBit a i
                      | otherwise = False
+  {-# INLINE testBit #-}
   bitSize = undefined
 #if MIN_VERSION_base(4,7,0)
   bitSizeMaybe = const Nothing
@@ -623,9 +729,11 @@
   shiftL (BV n a) k
     | k > n     = BV n 0
     | otherwise = BV n $ shiftL a k `mod` 2^n
+  {-# INLINE shiftL #-}
   shiftR (BV n a) k
     | k > n     = BV n 0
     | otherwise = BV n $ shiftR a k
+  {-# INLINE shiftR #-}
   rotateL bv       0 = bv
   rotateL (BV n a) k
     | k == n    = BV n a
@@ -634,6 +742,7 @@
     where s = n - k
           l = a `shiftR` s
           h = (a `shiftL` k) `mod` 2^n
+  {-# INLINE rotateL #-}
   rotateR bv       0 = bv
   rotateR (BV n a) k
     | k == n    = BV n a
@@ -642,7 +751,9 @@
     where s = n - k
           l = a `shiftR` k
           h = (a `shiftL` s) `mod` 2^n
+  {-# INLINE rotateR #-}
   popCount (BV _ a) = assert (a >= 0) $ popCount a
+  {-# INLINE popCount #-}
 
 -- | An alias for 'complement'.
 not, not_ :: BV -> BV
@@ -728,11 +839,12 @@
 -- >>> fromBits [False, False, True]
 -- [3]1
 fromBits :: [Bool] -> BV
-fromBits bs = BV n $ snd $ List.foldr go (1,0) bs
-  where n = List.length bs
-        go b (!v,!acc) | b         = (v',acc+v)
-                       | otherwise = (v',acc)
-          where v' = 2*v
+fromBits bs =
+  let (n,k) = List.foldr go (0,0) bs in
+  BV n k
+  -- NB: 'setBit' is a GMP function, faster than regular addition.
+  where go b (!i,!v) | b         = (i+1,setBit v i)
+                     | otherwise = (i+1,v)
 {-# INLINE fromBits #-}
 
 -- | Create a big-endian list of bits from a bit-vector.
@@ -783,10 +895,11 @@
 --- Utilities
 
 -- | Greatest natural number representable with /n/ bits.
-maxNat :: (Integral a, Integral b) => a -> b
+maxNat :: Integral size => size -> Integer
 maxNat n = 2^n - 1
 {-# INLINE maxNat #-}
 
+#ifndef MIN_VERSION_integer_gmp
 -- | Minimum width of a bit-vector to represent a given integer number.
 --
 -- >>> integerWith 4
@@ -801,3 +914,4 @@
   where go !k !k_max | k_max >= n = k
                      | otherwise  = go (k+1) (2*k_max+1)
 {-# INLINE integerWidth #-}
+#endif
diff --git a/test/Properties.hs b/test/Properties.hs
--- a/test/Properties.hs
+++ b/test/Properties.hs
@@ -6,7 +6,7 @@
 {-# LANGUAGE TupleSections     #-}
 
 -- |
--- Copyright : (c) 2012-2014 Iago Abal
+-- Copyright : (c) 2012-2016 Iago Abal
 --             (c) 2012-2013 HASLab & University of Minho
 -- License   : BSD3
 -- Maintainer: Iago Abal <mail@iagoabal.eu>
@@ -15,6 +15,7 @@
 module Main where
 
 import Data.BitVector as BV
+import Data.List as List
 
 import Control.Applicative ( (<$>), (<*>) )
 
@@ -32,6 +33,9 @@
 c_MAX_SIZE :: Int
 c_MAX_SIZE = 8192
 
+c_SMALL_NAT :: Int
+c_SMALL_NAT = 128
+
 data BV2 = BV2 !BV !BV
     deriving (Eq,Show)
 
@@ -41,8 +45,15 @@
 divides :: Integral a => a -> a -> Bool
 divides k n = n `mod` k == 0
 
+aNat :: Gen Int
+aNat = abs <$> arbitrary
+
+aSmallNat, anExp :: Gen Int
+aSmallNat = min c_SMALL_NAT <$> aNat
+anExp = aSmallNat
+
 gSize :: Gen Int
-gSize = min c_MAX_SIZE . (+1) . abs <$> arbitrary
+gSize = min c_MAX_SIZE . (+1) <$> aNat
 
 gBV :: Int -> Gen BV
 gBV sz = bitVec sz <$> choose (0::Integer,2^sz-1)
@@ -76,6 +87,12 @@
 
 -- * bitVec
 
+prop_bv_any :: Integer -> Property
+prop_bv_any i = forAll gSize $ \n ->
+  let u = bitVec n i in
+  let a = nat u in
+  a >= 0 && a < 2^n
+
 prop_bv_nat :: Integer -> Property
 prop_bv_nat i = i >= 0 ==> nat(fromInteger i) == i
 
@@ -84,6 +101,10 @@
 
 -- * Indexing
 
+prop_mult_index :: BV -> Property
+prop_mult_index a = forAll (listOf (gIndex a)) $ \is ->
+  a @: is ==. fromBits (List.map (a @.) is)
+
 prop_rev_index :: BV -> Property
 prop_rev_index a = forallIndexOf a $ \i -> a !. i == a @. (size(a)-i-1)
 
@@ -99,6 +120,13 @@
 prop_neg_id :: BV -> Bool
 prop_neg_id a = -(-a) ==. a
 
+prop_neg_int :: Integer -> Property
+prop_neg_int i = forAll gSize $ \n ->
+  let u = bitVec n i in
+  if nat u == 2^(n-1) -- only the msb is set, ie 1000...0
+  then int u == -2^(n-1) && int (-u) == int u -- overflow!
+  else int (-u) == -(int u)
+
 prop_abs_id :: BV -> Bool
 prop_abs_id a = abs(abs(a)) ==. abs(a)
 
@@ -142,6 +170,16 @@
 prop_smod_is_rem a b =
   isNat a && isPos b ==> a `smod` b ==. a `rem` b
 
+-- * Exponentiation
+
+prop_exp_zero :: BV -> Bool
+prop_exp_zero a =
+  pow a (0::Int) ==. bitVec (size a) (1::Int)
+
+prop_exp_spec :: BV -> Property
+prop_exp_spec a = forAll anExp $ \e ->
+  e /= 0 ==> pow a e ==. a^e
+
 -- * Not
 
 prop_not_id :: BV -> Bool
@@ -176,8 +214,7 @@
 
 prop_shr_div :: BV -> Property
 prop_shr_div a = forallIndex1Of a $ \i ->
-                   a `shiftR` i == a `div` bitVec n ((2::Integer)^i)
-  where n = size a
+                   a `shiftR` i == a `div` fromInteger((2::Integer)^i)
 
 -- * Rotate
 
@@ -187,6 +224,29 @@
 prop_ror_id :: BV -> Bool
 prop_ror_id a = a `rotateR` (size a) ==. a
 
+-- * Concat
+
+prop_concat_id :: BV -> Bool
+prop_concat_id a = nil # a ==. a && a # nil ==. a
+
+prop_concat_assoc :: BV -> BV -> BV -> Bool
+prop_concat_assoc a b c = (a # b) # c ==. a # (b # c)
+
+prop_concat_join :: [BV] -> Bool
+prop_concat_join us = join us ==. List.foldr (#) nil us
+
+-- * Bit extension
+
+prop_zero_extend :: BV -> Property
+prop_zero_extend a = forAll aNat $ \d ->
+  let a' = zeroExtend d a in
+  a' == a && size a' - size a == d
+
+prop_sign_extend :: BV -> Property
+prop_sign_extend a = forAll aSmallNat $ \d ->
+  let a' = signExtend d a in
+  int a' == int a && size a' - size a == d
+
 -- * Split & group
 
 prop_split_join_id :: BV -> Property
@@ -196,4 +256,3 @@
 prop_group_join_id :: BV -> Property
 prop_group_join_id a = forallDivisorOf (size a) $ \n ->
   BV.join (BV.group n a) ==. a
-