diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2014, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-containers.cabal b/liquid-containers.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-containers.cabal
@@ -0,0 +1,57 @@
+cabal-version:      1.24
+name:               liquid-containers
+version:            0.6.2.1
+synopsis:           LiquidHaskell specs for the containers package
+description:        LiquidHaskell specs for the containers package.
+license:            BSD3
+license-file:       LICENSE
+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
+author:             Ranjit Jhala, Niki Vazou, Eric Seidel
+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
+category:           Language
+homepage:           https://github.com/ucsd-progsys/liquidhaskell
+build-type:         Custom
+
+data-files:           src/Data/Set.spec
+
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
+library
+  exposed-modules:    Data.Containers.ListUtils
+                      Data.IntMap
+                      Data.IntMap.Lazy
+                      Data.IntMap.Strict
+                      Data.IntMap.Strict.Internal
+                      Data.IntMap.Internal
+                      Data.IntMap.Internal.Debug
+                      Data.IntMap.Merge.Lazy
+                      Data.IntMap.Merge.Strict
+                      Data.IntSet.Internal
+                      Data.IntSet
+                      Data.Map
+                      Data.Map.Lazy
+                      Data.Map.Merge.Lazy
+                      Data.Map.Strict.Internal
+                      Data.Map.Strict
+                      Data.Map.Merge.Strict
+                      Data.Map.Internal
+                      Data.Map.Internal.Debug
+                      Data.Set.Internal
+                      Data.Set
+                      Data.Graph
+                      Data.Sequence
+                      Data.Sequence.Internal
+                      Data.Sequence.Internal.Sorting
+                      Data.Tree
+                      Utils.Containers.Internal.BitUtil
+                      Utils.Containers.Internal.BitQueue
+                      Utils.Containers.Internal.StrictPair
+  hs-source-dirs:     src
+  build-depends:      liquid-base          < 5
+                    , containers           >= 0.6.2.1 && < 0.7
+                    , liquidhaskell        >= 0.8.10.1
+  default-language:   Haskell2010
+  default-extensions: PackageImports
+  if impl(ghc >= 8.10)
+    ghc-options: -fplugin=LiquidHaskell
diff --git a/src/Data/Containers/ListUtils.hs b/src/Data/Containers/ListUtils.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Containers/ListUtils.hs
@@ -0,0 +1,3 @@
+module Data.Containers.ListUtils (module Exports) where
+
+import "containers" Data.Containers.ListUtils as Exports
diff --git a/src/Data/Graph.hs b/src/Data/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Graph.hs
@@ -0,0 +1,3 @@
+module Data.Graph (module Exports) where
+
+import "containers" Data.Graph as Exports
diff --git a/src/Data/IntMap.hs b/src/Data/IntMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap.hs
@@ -0,0 +1,3 @@
+module Data.IntMap (module Exports) where
+
+import "containers" Data.IntMap as Exports
diff --git a/src/Data/IntMap/Internal.hs b/src/Data/IntMap/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Internal.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Internal (module Exports) where
+
+import "containers" Data.IntMap.Internal as Exports
diff --git a/src/Data/IntMap/Internal/Debug.hs b/src/Data/IntMap/Internal/Debug.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Internal/Debug.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Internal.Debug (module Exports) where
+
+import "containers" Data.IntMap.Internal.Debug as Exports
diff --git a/src/Data/IntMap/Lazy.hs b/src/Data/IntMap/Lazy.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Lazy.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Lazy (module Exports) where
+
+import "containers" Data.IntMap.Lazy as Exports
diff --git a/src/Data/IntMap/Merge/Lazy.hs b/src/Data/IntMap/Merge/Lazy.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Merge/Lazy.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Merge.Lazy (module Exports) where
+
+import "containers" Data.IntMap.Merge.Lazy as Exports
diff --git a/src/Data/IntMap/Merge/Strict.hs b/src/Data/IntMap/Merge/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Merge/Strict.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Merge.Strict (module Exports) where
+
+import "containers" Data.IntMap.Merge.Strict as Exports
diff --git a/src/Data/IntMap/Strict.hs b/src/Data/IntMap/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Strict.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Strict (module Exports) where
+
+import "containers" Data.IntMap.Strict as Exports
diff --git a/src/Data/IntMap/Strict/Internal.hs b/src/Data/IntMap/Strict/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntMap/Strict/Internal.hs
@@ -0,0 +1,3 @@
+module Data.IntMap.Strict.Internal (module Exports) where
+
+import "containers" Data.IntMap.Strict.Internal as Exports
diff --git a/src/Data/IntSet.hs b/src/Data/IntSet.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntSet.hs
@@ -0,0 +1,3 @@
+module Data.IntSet (module Exports) where
+
+import "containers" Data.IntSet as Exports
diff --git a/src/Data/IntSet/Internal.hs b/src/Data/IntSet/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IntSet/Internal.hs
@@ -0,0 +1,3 @@
+module Data.IntSet.Internal (module Exports) where
+
+import "containers" Data.IntSet.Internal as Exports
diff --git a/src/Data/Map.hs b/src/Data/Map.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map.hs
@@ -0,0 +1,3 @@
+module Data.Map ( module Exports ) where
+
+import "containers" Data.Map as Exports
diff --git a/src/Data/Map/Internal.hs b/src/Data/Map/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Internal.hs
@@ -0,0 +1,3 @@
+module Data.Map.Internal (module Exports) where
+
+import "containers" Data.Map.Internal as Exports
diff --git a/src/Data/Map/Internal/Debug.hs b/src/Data/Map/Internal/Debug.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Internal/Debug.hs
@@ -0,0 +1,3 @@
+module Data.Map.Internal.Debug (module Exports) where
+
+import "containers" Data.Map.Internal.Debug as Exports
diff --git a/src/Data/Map/Lazy.hs b/src/Data/Map/Lazy.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Lazy.hs
@@ -0,0 +1,3 @@
+module Data.Map.Lazy (module Exports) where
+
+import "containers" Data.Map.Lazy as Exports
diff --git a/src/Data/Map/Merge/Lazy.hs b/src/Data/Map/Merge/Lazy.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Merge/Lazy.hs
@@ -0,0 +1,3 @@
+module Data.Map.Merge.Lazy (module Exports) where
+
+import "containers" Data.Map.Merge.Lazy as Exports
diff --git a/src/Data/Map/Merge/Strict.hs b/src/Data/Map/Merge/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Merge/Strict.hs
@@ -0,0 +1,3 @@
+module Data.Map.Merge.Strict (module Exports) where
+
+import "containers" Data.Map.Merge.Strict as Exports
diff --git a/src/Data/Map/Strict.hs b/src/Data/Map/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Strict.hs
@@ -0,0 +1,3 @@
+module Data.Map.Strict (module Exports) where
+
+import "containers" Data.Map.Strict as Exports
diff --git a/src/Data/Map/Strict/Internal.hs b/src/Data/Map/Strict/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Map/Strict/Internal.hs
@@ -0,0 +1,3 @@
+module Data.Map.Strict.Internal (module Exports) where
+
+import "containers" Data.Map.Strict.Internal as Exports
diff --git a/src/Data/Sequence.hs b/src/Data/Sequence.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Sequence.hs
@@ -0,0 +1,3 @@
+module Data.Sequence (module Exports) where
+
+import "containers" Data.Sequence as Exports
diff --git a/src/Data/Sequence/Internal.hs b/src/Data/Sequence/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Sequence/Internal.hs
@@ -0,0 +1,3 @@
+module Data.Sequence.Internal (module Exports) where
+
+import "containers" Data.Sequence.Internal as Exports
diff --git a/src/Data/Sequence/Internal/Sorting.hs b/src/Data/Sequence/Internal/Sorting.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Sequence/Internal/Sorting.hs
@@ -0,0 +1,3 @@
+module Data.Sequence.Internal.Sorting (module Exports) where
+
+import "containers" Data.Sequence.Internal.Sorting as Exports
diff --git a/src/Data/Set.hs b/src/Data/Set.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Set.hs
@@ -0,0 +1,3 @@
+module Data.Set ( module Exports ) where
+
+import "containers" Data.Set as Exports
diff --git a/src/Data/Set.spec b/src/Data/Set.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/Set.spec
@@ -0,0 +1,59 @@
+module spec Data.Set where
+
+embed Data.Set.Internal.Set as Set_Set
+
+// ----------------------------------------------------------------------------------------------
+// -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
+// ----------------------------------------------------------------------------------------------
+
+
+// union
+measure Set_cup  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
+
+// intersection
+measure Set_cap  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
+
+// difference
+measure Set_dif   :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
+
+// singleton
+measure Set_sng   :: a -> (Data.Set.Internal.Set a)
+
+// emptiness test
+measure Set_emp   :: (Data.Set.Internal.Set a) -> GHC.Types.Bool
+
+// empty set
+measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a)
+
+// membership test
+measure Set_mem  :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
+
+// inclusion test
+measure Set_sub  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
+
+// ---------------------------------------------------------------------------------------------
+// -- | Refined Types for Data.Set Operations --------------------------------------------------
+// ---------------------------------------------------------------------------------------------
+
+isSubsetOf    :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y}
+member        :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs}
+null          :: (GHC.Classes.Ord a) => xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_emp xs}
+
+empty         :: {v:(Data.Set.Internal.Set a) | Set_emp v}
+singleton     :: x:a -> {v:(Data.Set.Internal.Set a) | v = (Set_sng x)}
+insert        :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs (Set_sng x)}
+delete        :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs (Set_sng x)}
+
+union         :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs ys}
+intersection  :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cap xs ys}
+difference    :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs ys}
+
+fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs}
+
+// ---------------------------------------------------------------------------------------------
+// -- | The set of elements in a list ----------------------------------------------------------
+// ---------------------------------------------------------------------------------------------
+
+measure listElts :: [a] -> (Data.Set.Internal.Set a)
+listElts([])   = {v | (Set_emp v)}
+listElts(x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
diff --git a/src/Data/Set/Internal.hs b/src/Data/Set/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Set/Internal.hs
@@ -0,0 +1,3 @@
+module Data.Set.Internal (module Exports) where
+
+import "containers" Data.Set.Internal as Exports
diff --git a/src/Data/Tree.hs b/src/Data/Tree.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Tree.hs
@@ -0,0 +1,3 @@
+module Data.Tree (module Exports) where
+
+import "containers" Data.Tree as Exports
diff --git a/src/Utils/Containers/Internal/BitQueue.hs b/src/Utils/Containers/Internal/BitQueue.hs
new file mode 100644
--- /dev/null
+++ b/src/Utils/Containers/Internal/BitQueue.hs
@@ -0,0 +1,3 @@
+module Utils.Containers.Internal.BitQueue (module Exports) where
+
+import "containers" Utils.Containers.Internal.BitQueue as Exports
diff --git a/src/Utils/Containers/Internal/BitUtil.hs b/src/Utils/Containers/Internal/BitUtil.hs
new file mode 100644
--- /dev/null
+++ b/src/Utils/Containers/Internal/BitUtil.hs
@@ -0,0 +1,3 @@
+module Utils.Containers.Internal.BitUtil (module Exports) where
+
+import "containers" Utils.Containers.Internal.BitUtil as Exports
diff --git a/src/Utils/Containers/Internal/StrictPair.hs b/src/Utils/Containers/Internal/StrictPair.hs
new file mode 100644
--- /dev/null
+++ b/src/Utils/Containers/Internal/StrictPair.hs
@@ -0,0 +1,3 @@
+module Utils.Containers.Internal.StrictPair (module Exports) where
+
+import "containers" Utils.Containers.Internal.StrictPair as Exports