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 774C77FA1F for ; Tue, 22 Jul 2014 00:37:48 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oliver@first.in-berlin.de) identity=pra; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="oliver@first.in-berlin.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oliver@first.in-berlin.de) identity=mailfrom; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="oliver@first.in-berlin.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@einhorn.in-berlin.de) identity=helo; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="postmaster@einhorn.in-berlin.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArABAOCVzVPAbSoIf2dsb2JhbABZg2BXBIJ0xAiHQwGBFxYPAQELCwoIFCmEBAEEASMPAQUwFgsLGgIYDgICVxmIOggECagSlzyBLI4mFoJiNoEYBZskgU6FQ4tGhR9q X-IPAS-Result: ArABAOCVzVPAbSoIf2dsb2JhbABZg2BXBIJ0xAiHQwGBFxYPAQELCwoIFCmEBAEEASMPAQUwFgsLGgIYDgICVxmIOggECagSlzyBLI4mFoJiNoEYBZskgU6FQ4tGhR9q X-IronPort-AV: E=Sophos;i="5.01,705,1400018400"; d="scan'208";a="86366479" Received: from einhorn.in-berlin.de ([192.109.42.8]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 22 Jul 2014 00:37:47 +0200 X-Envelope-From: oliver@first.in-berlin.de X-Envelope-To: Received: from yak (yak.in-berlin.de [192.109.42.109]) by einhorn.in-berlin.de (8.14.4/8.14.4/Debian-4) with ESMTP id s6LMbkvw028204 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Tue, 22 Jul 2014 00:37:46 +0200 Received: from e178021156.adsl.alicedsl.de (e178021156.adsl.alicedsl.de [85.178.21.156]) by webmail.in-berlin.de (Horde Framework) with HTTP; Tue, 22 Jul 2014 00:37:45 +0200 Date: Tue, 22 Jul 2014 00:37:45 +0200 Message-ID: <20140722003745.Horde.c4SRKyZgSXOQILb6jBJVpA1@webmail.in-berlin.de> From: Oliver Bandel To: caml-list@inria.fr References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> <53CAC46C.2010905@linux-france.org> In-Reply-To: <53CAC46C.2010905@linux-france.org> User-Agent: Internet Messaging Program (IMP) H5 (6.2.0) Content-Type: text/plain; charset=UTF-8; format=flowed; DelSp=Yes MIME-Version: 1.0 Content-Disposition: inline Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Program proof - how to do that? Hello, thanks to all people who answered. I'm sorry that I can't attend to the logics conference mentioned in on answer. Maybe next time. Would be fine if such events could be mentioned on this list. Zitat von David MENTRÉ (Sat, 19 Jul 2014 21:18:04 +0200) > Hello Gabriel, > > 2014-07-12 14:07, Gabriel Scherer: >> I tried to (partially) answer this question in the following >> StackOverflow thread: >> http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations > > > Nice answer. > > BTW, regarding Why3 in your answer, the current git version of Why3 > allows to produce OCaml code from a proved WhyML program, [...] I here now do hear the first time about "Why3". Interesting to see what is available in the area of program proof. But my question also was about the theoretical background of the proof stuff. For example in my exploration of logics I came across model theory and tarski semantics. Looks interesting to me, something worth exploring in more detail, I think. Does anybody know more about these topics (theoretically as well as if this is used in theorem provers)? Ciao, Oliver