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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 6FF317EE4B for ; Tue, 8 Oct 2013 15:27:55 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rj@robertjakob.de) identity=pra; client-ip=37.59.40.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rj@robertjakob.de"; x-sender="rj@robertjakob.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rj@robertjakob.de) identity=mailfrom; client-ip=37.59.40.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rj@robertjakob.de"; x-sender="rj@robertjakob.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@robertjakob.de) identity=helo; client-ip=37.59.40.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rj@robertjakob.de"; x-sender="postmaster@robertjakob.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj4GANkHVFIlOygyX2dsb2JhbABZFoMps3yIPIU8CoErAx9SgiUBAQQBOkQLCyElDxIiFBmHdAMJBgQIsFENiWuMV4JyFhiDdQOUJBiBXIFojEuIXA X-IPAS-Result: Aj4GANkHVFIlOygyX2dsb2JhbABZFoMps3yIPIU8CoErAx9SgiUBAQQBOkQLCyElDxIiFBmHdAMJBgQIsFENiWuMV4JyFhiDdQOUJBiBXIFojEuIXA X-IronPort-AV: E=Sophos;i="4.90,1056,1371074400"; d="scan'208";a="29528561" Received: from ks3000501.kimsufi.com (HELO robertjakob.de) ([37.59.40.50]) by mail3-smtp-sop.national.inria.fr with ESMTP; 08 Oct 2013 15:27:54 +0200 Received: from jakobro-VirtualBox (c166188.informatik.uni-freiburg.de [132.230.166.188]) by robertjakob.de (Postfix) with ESMTPSA id 427648131D for ; Tue, 8 Oct 2013 15:27:53 +0200 (CEST) Date: Tue, 8 Oct 2013 15:27:53 +0200 From: Robert Jakob To: caml-list@inria.fr Message-ID: <20131008152753.43eb5a2f@jakobro-VirtualBox> In-Reply-To: References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn> <20130929165650.34da2e99@oberon> <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> <20130930145358.GF8693@frosties> X-Mailer: Claws Mail 3.9.1 (GTK+ 2.24.13; x86_64-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] equivalent checking of ocaml program? On Mon, 30 Sep 2013 17:49:11 +0200 Gabriel Scherer wrote: > This thread may be a good opportunity to advertize for some work on > static program verification that has been applied to OCaml (sadly, it > is actually quite rare to see program verification efforts for > functional programming languages, in large part because funding > bodies and reviewers appreciate applications to mainstream language > with larger codebases). I am aware of the following, feel free to add > more suggestions: > - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/ > Based on foundational work on model-checking of higher-order > programs by Ong, Kobayashi and others (see the citations of the > papers on the webpage), MoCHi can work with a subset of OCaml. It is > not ready to handle real-world programs, both in term of verification > time and the ocaml feature it understands, but going in the right > direction -- and the underlying tools are rapidly improving, see e.g. > the recent work on C-SHORe The approaches by Ong, Kobayashi, Broadbent et al. work on higher-order recursion schemes (HORS) to represent output/states of functional programs. Yet, it is not known if the equivalence of two HORS is decidable. So this might be applicable to deciding the equivalency of ocaml programs (wrt. outputs/state), but it is not clear. r.