From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 249687F927 for ; Tue, 10 Jun 2014 20:19:07 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.98,1010,1392159600"; d="scan'208";a="79393949" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 10 Jun 2014 20:19:07 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 154F37F929; Tue, 10 Jun 2014 20:19:07 +0200 (CEST) Date: Tue, 10 Jun 2014 20:19:05 +0200 To: Xavier.Leroy@inria.fr,caml-list@inria.fr In-Reply-To: <538CAD12.2040104@inria.fr> Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: 7BIT From: X-Mailer: Sympa 6.1.17 Subject: Re: [Caml-list] Why AVL-tree? I am coming here from the Coq mailing list, because of a link posted there about this e-mail thread. I have been working on Coq-verified and fully proof-erased versions of AVL and red-black trees, as well as a variant I didn't know existed before, until I read about "2-imbalance AVL trees" in this thread. The github address for my development is: https://github.com/jonleivent/mindless-coding and the "gaptree" development there may be the same as your "2-imbalance" AVL trees, though I can't be sure without more of an explanation (or maybe just a pointer to the source code) for the 2-imbalance AVL trees. Any further information or source pointers you can give me would be greatly appreciated. Thanks --Jonathan