From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 43B207F730 for ; Thu, 16 Mar 2017 14:53:35 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hendrik@topoi.pooq.com; spf=None smtp.mailfrom=hendrik@topoi.pooq.com; spf=None smtp.helo=postmaster@april.topoi.pooq.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of hendrik@topoi.pooq.com) identity=pra; client-ip=69.165.131.134; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hendrik@topoi.pooq.com"; x-sender="hendrik@topoi.pooq.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of hendrik@topoi.pooq.com) identity=mailfrom; client-ip=69.165.131.134; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hendrik@topoi.pooq.com"; x-sender="hendrik@topoi.pooq.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@april.topoi.pooq.com) identity=helo; client-ip=69.165.131.134; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hendrik@topoi.pooq.com"; x-sender="postmaster@april.topoi.pooq.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AUAxY9BY8/8pf8h6fcNJPW6f/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZr8+4bnLW6fgltlLVR4KTs6sC0LuL9f64Ejdaqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjSwbLdyIRmsrAjdqsYajIV8Jq0s1hbHv3xEdv?= =?us-ascii?q?hMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTD?= =?us-ascii?q?QhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlS?= =?us-ascii?q?AIOSMk8GHMksx/kr5UoA6vqRx4xo7beoCVNPxjda/Zct4XQW9NU8BMXCJDH4y8?= =?us-ascii?q?dZMCAeQBM+hGsofzpFUOohSiCgaxBuzgxCRFhmPq0aAgz+gtDRvL0BImEtkTsH?= =?us-ascii?q?rUttL1NKIKXO630qbIyyjMb+lX2Tf+9YPFbxchofaJXbltdsfRyVcgFwXYgVWK?= =?us-ascii?q?qIzlPCiY1vgKs2iD6OpgVPiji3YgqwF2uzij3Nsjio7Mho8MzF3P6Ct3wIEwJd?= =?us-ascii?q?KiSU57Z8apEJpWtyGANot5WNkuQ29yuCoixb0GuIK7fCgXyJs83RLQd/uHc42Q?= =?us-ascii?q?7hPjTumRITB4hHV/dL2jgBay9E6twfD/WMmsyFtHry5InsPRun0M1xHf8NWLR/?= =?us-ascii?q?Vg8ku7xDqC2Q/e5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3sg6+ObEUk++yo?= =?us-ascii?q?5/77YrXhvp+cMI50hhvmMqQpncy/GP40PRQJX2ie4ei81bvj8lPlQLhSj/A7lr?= =?us-ascii?q?PVvI3bKMkbvKK1HgFY3ps55xqiATqr38wUnXwdI1JEfBKHgZLpO1bLIP3gDfew?= =?us-ascii?q?nVKsnypxx/DHPb3sGYnNLn/bkLfmfLZx8VZcyA00zdBG/Z5bFrYBIPfrVk/rqN?= =?us-ascii?q?PYFgM5MxCzw+v/FNpyzIYeWWaWDq+dMaPSqkOI6/k0I+iMYY8VoCzyJ+Ik5/7o?= =?us-ascii?q?l385mEUScbOn3ZsNOziEGaFtKkCdJH7tmcspEGEQvwN4Qva5pkeFVGtzanC+Ra?= =?us-ascii?q?M/rhs8D4fuWYfOQIy3gb+pwCCjGZwQfmdBExaHFnK+JNbMYOsFdC/HepwpqTcD?= =?us-ascii?q?T7X0F94s?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BzAgAgmMpY/4aDpUVeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhAeBC4MSil1zkGWCOpMFgg4qhXgCg0IYAQEBAQEBAQEBAQFqKII?= =?us-ascii?q?zCoJYAQEBAQIBOjQbCxgJBCEPBRgZPYlWAw0IDrJ/hzgDgxgBAQEHAgEliz2EQ?= =?us-ascii?q?GCCaIIxBYdADJR5hneLOg1pgWaOWpNNHziBBCMWCBcVQYZzJIdBgjwBAQE?= X-IPAS-Result: =?us-ascii?q?A0BzAgAgmMpY/4aDpUVeHAEBBAEBCgEBFwEBBAEBCgEBhAe?= =?us-ascii?q?BC4MSil1zkGWCOpMFgg4qhXgCg0IYAQEBAQEBAQEBAQFqKIIzCoJYAQEBAQIBO?= =?us-ascii?q?jQbCxgJBCEPBRgZPYlWAw0IDrJ/hzgDgxgBAQEHAgEliz2EQGCCaIIxBYdADJR?= =?us-ascii?q?5hneLOg1pgWaOWpNNHziBBCMWCBcVQYZzJIdBgjwBAQE?= X-IronPort-AV: E=Sophos;i="5.36,172,1486422000"; d="scan'208";a="216983338" Received: from topoi.pooq.com (HELO april.topoi.pooq.com) ([69.165.131.134]) by mail3-smtp-sop.national.inria.fr with ESMTP; 16 Mar 2017 14:53:33 +0100 Received: by april.topoi.pooq.com (Postfix, from userid 1001) id E8809C202A; Thu, 16 Mar 2017 09:53:31 -0400 (EDT) Date: Thu, 16 Mar 2017 09:53:31 -0400 From: Hendrik Boom To: caml-list@inria.fr Message-ID: <20170316135331.GA21804@topoi.pooq.com> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] Preview: B-tree library On Thu, Mar 16, 2017 at 01:35:26PM +0000, Tom Ridge wrote: > Dear All, > > This may be of interest for people thinking about on-disk storage etc. > > https://github.com/tomjridge/tjr_btree/ > > It is not really in state to release, hence the "preview". > > It is the core library in the upcoming "ImpFS" filesystem which (with > SibylFS) comes from the "Future filesystems" project. The intereseting point about this syste is in the README: tjr_btree is a B-tree library. The core is written in Isabelle/HOL and exported to OCaml Does this mean something like that the code has been generated from a ormal proof of its correctness? -- hendrik > > Thanks > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs