From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 A02CB7F730 for ; Thu, 16 Mar 2017 18:48:39 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=parsert.julian@gmail.com; spf=Pass smtp.mailfrom=parsert.julian@gmail.com; spf=None smtp.helo=postmaster@mail-wr0-f195.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of parsert.julian@gmail.com) identity=pra; client-ip=209.85.128.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="parsert.julian@gmail.com"; x-sender="parsert.julian@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of parsert.julian@gmail.com designates 209.85.128.195 as permitted sender) identity=mailfrom; client-ip=209.85.128.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="parsert.julian@gmail.com"; x-sender="parsert.julian@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wr0-f195.google.com) identity=helo; client-ip=209.85.128.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="parsert.julian@gmail.com"; x-sender="postmaster@mail-wr0-f195.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AynugaBZJBaZ17PyF/RaDuwf/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZpsWybnLW6fgltlLVR4KTs6sC0LuL9f64EjNRqdbZ6TZZL8wKD0dEwe?= =?us-ascii?q?wt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYn?= =?us-ascii?q?br+tQt2auf+qzPi/8IH/ZABBhTz1Ie8jbUb+kQKEvcAThc5mK70t4hrPuHpBPe?= =?us-ascii?q?pMlk1yIlfGvQv45862tKZq6T9doe5po9ZJS773Zbh+T6FcDT0gG28w7czv8xLE?= =?us-ascii?q?SF3ctTMnTmwKn08QUED+5xbgU8Kt4yY=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AlAwAqz8pYf8OAVdFeHAEBBAEBCgEBF?= =?us-ascii?q?QEBAQECAQEBAQgBAQEBhAcDJ2CfKR+COoZEjk8qhXgCgwZCFQEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBCQsLCCYxgjMEAwMdgjwBAgM4CAEbEgwDDAYFCw0NISMRAQUBChITCAEBD?= =?us-ascii?q?olVAQMVBAqkaT+OBwUBHIMJBYNcChknAwpVgjkBAQEBAQUBAQEBAQEaAgYJAQi?= =?us-ascii?q?IQQiCYoRAYIUZBYdADJR5hneLR2iBZ4d4D4ZTkgUzgRU1gSYjFh9WF4QxghB0h?= =?us-ascii?q?wyBAYE7AQEB?= X-IPAS-Result: =?us-ascii?q?A0AlAwAqz8pYf8OAVdFeHAEBBAEBCgEBFQEBAQECAQEBAQg?= =?us-ascii?q?BAQEBhAcDJ2CfKR+COoZEjk8qhXgCgwZCFQEBAQEBAQEBAQEBEgEBCQsLCCYxg?= =?us-ascii?q?jMEAwMdgjwBAgM4CAEbEgwDDAYFCw0NISMRAQUBChITCAEBDolVAQMVBAqkaT+?= =?us-ascii?q?OBwUBHIMJBYNcChknAwpVgjkBAQEBAQUBAQEBAQEaAgYJAQiIQQiCYoRAYIUZB?= =?us-ascii?q?YdADJR5hneLR2iBZ4d4D4ZTkgUzgRU1gSYjFh9WF4QxghB0hwyBAYE7AQEB?= X-IronPort-AV: E=Sophos;i="5.36,173,1486422000"; d="scan'208";a="264900169" Received: from mail-wr0-f195.google.com ([209.85.128.195]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 16 Mar 2017 18:47:54 +0100 Received: by mail-wr0-f195.google.com with SMTP id u108so6819251wrb.2 for ; Thu, 16 Mar 2017 10:47:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding; bh=I7u+UE2Y2NIUtL+m6CLzsrl7v7FP5e0M1kOmNN8lB5c=; b=NCs3B1OMTPiqBGaSAl0a5WmfIlGl3rHbwJm/CmdTpUs9yNV/+I9rwXq9K3cVZe3lCH sJnmsT6UmMShJeNawN1NrL9BFdTeEs0kSC6zBiqZBjgM9NCG0Fspu2biDs0bhA89ycI5 vFj0BgC9lvnbYZvM6+WPNR+CHP4K1I3j67EaX8F70pDmygb3sZclyO2STOjj79RDsXLj ii/665WUzp4laM2qGUzuhw/IwLibpI1/MNpOK9UaJJeVBoPuJSFyK3B7ceQfNYHW4svX GRv1GZp6k2e6/hyCqXRd81B/ak4ueyJIxPmQnc/XMOcQmNbNxTy0qx00RQn6ACSj9ffB Tngg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-transfer-encoding; bh=I7u+UE2Y2NIUtL+m6CLzsrl7v7FP5e0M1kOmNN8lB5c=; b=aacpBMrYMeb3LLjiEfVz8qf9jxJL1A5e3SozrZkWUiPGRXbgZz3ihN4fnic/ZaKtqM DF/3VQDzoV9++jQ5lmb65FDSbVZXScIaEtA0sR23+PEIQ7TqaKUAJ06JxOKUMtCOXLyr CUKERDxwWK3hl1jrNsOrZIk4+bGjsMmjEINSbMiu3/8ag+4NWOYXdn1YjfRrjUdZ5ty3 x/jSpUw2h9JTqBEUof9au1Ua5yimkEMzXfCdZAyPtzxgvbOAuRpQE2WEOSSl2wD5692g VapudRRdFgbP1XtZisEM5YYUb/huMO0O+2VEDI2g5VITAUrqZXiPX9SvMh9h5W9oEmo4 Q0+A== X-Gm-Message-State: AFeK/H1aaDuFpac36gvlD6z5Mu3KGyjbDTsL2oKGWteo193rybERzPeL05nYtKFeEW/rtQ== X-Received: by 10.223.142.201 with SMTP id q67mr8637314wrb.182.1489686473556; Thu, 16 Mar 2017 10:47:53 -0700 (PDT) Received: from [192.168.178.63] (212-197-147-46.adsl.highway.telekom.at. [212.197.147.46]) by smtp.gmail.com with ESMTPSA id 191sm5112601wmo.21.2017.03.16.10.47.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Mar 2017 10:47:52 -0700 (PDT) To: caml-list@inria.fr References: <20170316135331.GA21804@topoi.pooq.com> From: Julian Parsert Message-ID: Date: Thu, 16 Mar 2017 18:47:51 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0 MIME-Version: 1.0 In-Reply-To: <20170316135331.GA21804@topoi.pooq.com> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Preview: B-tree library Or does anyone know where the core in Isabelle/HOL can be found? On 2017-03-16 14:53, Hendrik Boom wrote: > 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