diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 470dec0fa..0c763b2f8 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -25,3 +25,6 @@ add_test(scoped_map ${CMAKE_CURRENT_BINARY_DIR}/scoped_map)
 add_executable(thread thread.cpp)
 target_link_libraries(thread ${EXTRA_LIBS})
 add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread)
+add_executable(queue queue.cpp)
+target_link_libraries(queue ${EXTRA_LIBS})
+add_test(queue ${CMAKE_CURRENT_BINARY_DIR}/queue)
diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index 95de1cd4a..0fc938943 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -71,8 +71,7 @@ static void tst5() {
         auto p = split(l);
         list<int> l2 = append(p.first, p.second);
         lean_assert(l2 == l);
-        int diff = static_cast<int>(length(p.first)) - static_cast<int>(length(p.second));
-        lean_assert(-1 <= diff && diff <= 1);
+        lean_assert(-1 <= static_cast<int>(length(p.first)) - static_cast<int>(length(p.second)) && static_cast<int>(length(p.first)) - static_cast<int>(length(p.second)) <= 1);
     }
 }
 
diff --git a/src/tests/util/queue.cpp b/src/tests/util/queue.cpp
new file mode 100644
index 000000000..b2ebba3b0
--- /dev/null
+++ b/src/tests/util/queue.cpp
@@ -0,0 +1,130 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <cstdlib>
+#include <deque>
+#include "test.h"
+#include "queue.h"
+using namespace lean;
+
+/**
+   \brief Naive equality test for debugging
+*/
+template<typename T>
+bool operator==(queue<T> q1, queue<T> q2) {
+    while (!is_empty(q1) && !is_empty(q2)) {
+        auto p1 = pop_front(q1);
+        auto p2 = pop_front(q2);
+        if (p1.second != p2.second)
+            return false;
+        q1 = p1.first;
+        q2 = p2.first;
+    }
+    return is_empty(q1) && is_empty(q2);
+}
+
+
+template<typename T>
+bool operator==(queue<T> q1, std::deque<T> const & q2) {
+    for (auto v : q2) {
+        if (is_empty(q1))
+            return false;
+        auto p = pop_front(q1);
+        if (p.second != v)
+            return false;
+        q1 = p.first;
+    }
+    return is_empty(q1);
+}
+
+static void tst1() {
+    queue<int> q;
+    lean_assert(is_empty(q));
+    q = push_back(q, 1);
+    lean_assert(pop_front(q).second == 1);
+    lean_assert(pop_back(q).second  == 1);
+    lean_assert(!is_empty(q));
+    q = push_back(q, 2);
+    q = push_front(q, 3);
+    lean_assert(size(q) == 3);
+    lean_assert(pop_front(q).second == 3);
+    lean_assert(pop_back(q).second == 2);
+    lean_assert(pop_front(q).first.size() == 2);
+    std::cout << "q: " << q << "\n";
+    std::cout << "pop_front(q): " << pop_front(q).first << "\n";
+    lean_assert(pop_front(pop_front(q).first).second == 1);
+    lean_assert(pop_front(pop_front(pop_front(q).first).first).second == 2);
+    lean_assert(pop_front(pop_front(pop_front(q).first).first).first.is_empty());
+    lean_assert(pop_front(push_front(q, 3)).first == q);
+    lean_assert(pop_back(push_back(q, 3)).first == q);
+}
+
+static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq) {
+    std::deque<int> q1;
+    queue<int>      q2;
+    for (unsigned i = 0; i < num_ops; i++) {
+        double f = static_cast<double>(std::rand() % 10000) / 10000.0;
+        if (f < push_freq) {
+            if (q1.size() >= max_sz)
+                continue;
+            int v = std::rand() % max_val;
+            if (std::rand() % 2 == 0) {
+                q1.push_front(v);
+                lean_assert(pop_front(push_front(q2, v)).first == q2);
+                q2 = push_front(q2, v);
+            } else {
+                q1.push_back(v);
+                lean_assert(pop_back(push_back(q2, v)).first == q2);
+                q2 = push_back(q2, v);
+            }
+        } else {
+            if (q1.size() == 0)
+                continue;
+            if (std::rand() % 2 == 0) {
+                auto p = pop_front(q2);
+                lean_assert(p.second == q1.front());
+                q1.pop_front();
+                q2 = p.first;
+            } else {
+                auto p = pop_back(q2);
+                lean_assert(p.second == q1.back());
+                q1.pop_back();
+                q2 = p.first;
+            }
+        }
+        lean_assert(q2 == q1);
+    }
+}
+
+static void tst2() {
+    driver(4,  32, 10000, 0.5);
+    driver(2,  32, 10000, 0.8);
+    driver(2,  32, 10000, 0.3);
+    driver(4,  32, 10000, 0.3);
+    driver(16, 32, 10000, 0.5);
+    driver(16, 32, 10000, 0.7);
+    driver(16, 32, 10000, 0.1);
+    driver(16, 32, 10000, 0.8);
+    driver(16, 1000, 10000, 0.8);
+    driver(128, 1000, 10000, 0.5);
+    driver(128, 1000, 10000, 0.2);
+}
+
+static void tst3() {
+    queue<int> q{1, 2, 3, 4};
+    lean_assert(size(q) == 4);
+    lean_assert(pop_back(q).second == 4);
+    lean_assert(pop_front(q).second == 1);
+    lean_assert(pop_front(pop_front(q).first).second == 2);
+    lean_assert(pop_back(pop_back(q).first).second == 3);
+}
+
+int main() {
+    tst1();
+    tst2();
+    tst3();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/queue.h b/src/util/queue.h
new file mode 100644
index 000000000..025f3aac7
--- /dev/null
+++ b/src/util/queue.h
@@ -0,0 +1,127 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "list_fn.h"
+
+namespace lean {
+/**
+   \brief Functional queue
+*/
+template<typename T>
+class queue {
+    list<T> m_front;
+    list<T> m_rear;
+    queue(list<T> const & f, list<T> const & r):m_front(f), m_rear(r) {}
+public:
+    queue() {}
+    queue(unsigned num, T const * as) { m_front = to_list(as, as + num); }
+    queue(std::initializer_list<T> const & l):queue(l.size(), l.begin()) {}
+
+    /** \brief Return true iff the list is empty (complexity O(1)) */
+    bool is_empty() const { return is_nil(m_front) && is_nil(m_rear); }
+
+    /** \brief Return the size of the queue (complexity O(n)) */
+    unsigned size() const { return length(m_front) + length(m_rear); }
+
+    /** \brief Return the queue <tt>(v :: q)</tt> (complexity O(1)) */
+    friend queue push_front(queue const & q, T const & v) { return queue(cons(v, q.m_front), q.m_rear); }
+
+    /** \brief Return the queue <tt>(q :: v)</tt> (complexity O(1)) */
+    friend queue push_back(queue const & q, T const & v) { return queue(q.m_front, cons(v, q.m_rear)); }
+
+    /**
+        \brief Return the pair <tt>(q, v)</tt> for a queue <tt>(v :: q)</tt>.
+        Complexity: worst case is O(n), average O(1)
+
+        \pre !is_empty(q)
+    */
+    friend std::pair<queue, T> pop_front(queue const & q) {
+        lean_assert(!q.is_empty());
+        if (is_nil(q.m_front)) {
+            if (is_nil(cdr(q.m_rear))) {
+                return mk_pair(queue(), car(q.m_rear));
+            } else {
+                auto p = split(q.m_rear);
+                p.second = reverse(p.second);
+                return mk_pair(queue(cdr(p.second), p.first), car(p.second));
+            }
+        } else {
+            return mk_pair(queue(cdr(q.m_front), q.m_rear), car(q.m_front));
+        }
+    }
+
+    /**
+        \brief Return the pair <tt>(q, v)</tt> for a queue <tt>(q :: v)</tt>.
+        Complexity: worst case is O(n), average O(1)
+
+        \pre !is_empty(q)
+    */
+    friend std::pair<queue, T> pop_back(queue const & q) {
+        lean_assert(!q.is_empty());
+        if (is_nil(q.m_rear)) {
+            if (is_nil(cdr(q.m_front))) {
+                return mk_pair(queue(), car(q.m_front));
+            } else {
+                auto p = split(q.m_front);
+                p.second = reverse(p.second);
+                return mk_pair(queue(p.first, cdr(p.second)), car(p.second));
+            }
+        } else {
+            return mk_pair(queue(q.m_front, cdr(q.m_rear)), car(q.m_rear));
+        }
+    }
+
+    class iterator {
+        typename list<T>::iterator m_it;
+        queue const *              m_queue;
+        iterator(typename list<T>::iterator const & it, queue const * queue) {}
+    public:
+        iterator(iterator const & s):m_it(s.m_it), m_queue(s.m_queue) {}
+        iterator & operator++() {
+            ++m_it;
+            if (m_queue && m_it == m_queue->m_front.end()) {
+                m_it    = m_queue->m_rear.begin();
+                m_queue = nullptr;
+            }
+            return *this;
+        }
+        iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; }
+        bool operator==(iterator const & s) const { return m_it == s.m_it; }
+        bool operator!=(iterator const & s) const { return !operator==(s); }
+        T const & operator*() { return m_it.operator*(); }
+        T const * operator->() { return m_it.operator->(); }
+    };
+
+    /**
+        \brief Return an iterator for the beginning of the queue.
+        The iterator traverses the queue in an arbitrary order.
+    */
+    iterator begin() const { return iterator(m_front.begin(), this); }
+    iterator end() const { return iterator(m_rear.end(), nullptr); }
+};
+/** \brief Return the size of \c q. */
+template<typename T> unsigned size(queue<T> const & q) { return q.size(); }
+/** \brief Return true iff \c q is empty */
+template<typename T> bool is_empty(queue<T> const & q) { return q.is_empty(); }
+
+template<typename T> inline std::ostream & operator<<(std::ostream & out, queue<T> const & q) {
+    out << "[";
+    queue<T> q2 = q;
+    bool first = true;
+    while(!is_empty(q2)) {
+        auto p = pop_front(q2);
+        if (first)
+            first = false;
+        else
+            out << " ";
+        out << p.second;
+        q2 = p.first;
+    }
+    out << "]";
+    return out;
+}
+}