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 278D17FA1F for ; Tue, 22 Jul 2014 10:26:00 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of nmpgaspar@gmail.com) identity=pra; client-ip=209.85.219.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nmpgaspar@gmail.com"; x-sender="nmpgaspar@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of nmpgaspar@gmail.com designates 209.85.219.44 as permitted sender) identity=mailfrom; client-ip=209.85.219.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nmpgaspar@gmail.com"; x-sender="nmpgaspar@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-oa0-f44.google.com) identity=helo; client-ip=209.85.219.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nmpgaspar@gmail.com"; x-sender="postmaster@mail-oa0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuUDAHEfzlPRVdssm2dsb2JhbABYg2BXBIJ0gRyBRKt/MoNmjz2BY4dDAYEICBYPAQEBAQEGCwsJFCmEBAEBAwESER0BGwwCBAsBAwELBgULGh0CAiIBEQEFAQoSBhMICgcJiAsBAwkIDZteaosogXKDEIpHChknAwpkhiQRAQUOjzkEB4J4gU4BBIRwBYlPjGKBTZBxGCmCdYIBOy8 X-IPAS-Result: AuUDAHEfzlPRVdssm2dsb2JhbABYg2BXBIJ0gRyBRKt/MoNmjz2BY4dDAYEICBYPAQEBAQEGCwsJFCmEBAEBAwESER0BGwwCBAsBAwELBgULGh0CAiIBEQEFAQoSBhMICgcJiAsBAwkIDZteaosogXKDEIpHChknAwpkhiQRAQUOjzkEB4J4gU4BBIRwBYlPjGKBTZBxGCmCdYIBOy8 X-IronPort-AV: E=Sophos;i="5.01,708,1400018400"; d="scan'208";a="72362249" Received: from mail-oa0-f44.google.com ([209.85.219.44]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Jul 2014 10:25:58 +0200 Received: by mail-oa0-f44.google.com with SMTP id eb12so9281453oac.31 for ; Tue, 22 Jul 2014 01:25:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=QlTU34gMLypzyJcA/krHG24wTBbE7daW2pmgJa3WISs=; b=PmBnYx4Jjg+PhiWhQWxCwZ8I8lQ2tzlT8Np6uPJmFI0r4uhRYv7hchdiyOtr80r47w lWWvUrV+yptz95dIfk/TheyS6MMpA0u4K6iJopHp4gbEzL9G5U9+XLn900lHLN7rgMth oitZi8NQzwB9f+cFjVeMqIQAu8fxLKDWm5Vx2lPlo5ldni3H9rpP41bXL4iy3ieTEb/L i9BSmMSrPMlqXLvlpHyjnSTnj87pUPtpRgECIetV1FtFhFKbltQ5G/rzN/PmWoQrfM/R /kPffH0bSys4voNqNeI/aRuMu7j36P5bahoPWs7N2obZZOeDZ4yEHgKyNgMSiFA0cR98 Fn7w== MIME-Version: 1.0 X-Received: by 10.60.120.98 with SMTP id lb2mr45628631oeb.52.1406017555697; Tue, 22 Jul 2014 01:25:55 -0700 (PDT) Received: by 10.76.100.83 with HTTP; Tue, 22 Jul 2014 01:25:55 -0700 (PDT) In-Reply-To: <20140722003745.Horde.c4SRKyZgSXOQILb6jBJVpA1@webmail.in-berlin.de> References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> <53CAC46C.2010905@linux-france.org> <20140722003745.Horde.c4SRKyZgSXOQILb6jBJVpA1@webmail.in-berlin.de> Date: Tue, 22 Jul 2014 10:25:55 +0200 Message-ID: From: Nuno Gaspar To: Oliver Bandel Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=047d7b339dbdf4f64804fec3f8f4 Subject: Re: [Caml-list] Program proof - how to do that? --047d7b339dbdf4f64804fec3f8f4 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable You wanna take a look at Hoare Logic: http://en.wikipedia.org/wiki/Hoare_logic Then, you can peek Weakest precondiction calculus: http://en.wikipedia.org/wiki/Predicate_transformer_semantics And if you're brave, Separation logic. http://en.wikipedia.org/wiki/Separation_logic Oh, and if you still some more spare time: Rely/Guarantee. :) Hope it helps. 2014-07-22 0:37 GMT+02:00 Oliver Bandel : > 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=C3=89 (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 thin= k. > > Does anybody know more about these topics (theoretically as well as > if this is used in theorem provers)? > > > Ciao, > Oliver > > > > > > -- > 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 > --=20 Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year. Marge: Bart! Don't make fun of grad students, they just made a terrible life choice. --047d7b339dbdf4f64804fec3f8f4 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
You wanna take a look at Hoare Logic:=C2=A0http://en.wikipedia.org/wiki/Hoare_lo= gic

Then, you can peek Weakest precondiction calculu= s:=C2=A0http://en.wikipedia.org/wiki/Predicate_transformer_semantics

And if you're brave, Separation logic.
http://en.wikipedia= .org/wiki/Separation_logic

Oh, and if you = still some more spare time: Rely/Guarantee. :)

Hope it helps.


=


2014-07-22 0:37 GMT+02:00 Oliver Bandel <oliver@first.in-berlin= .de>:
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=C3=89 <dmentre@linux-france.org> (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:
=C2=A0 http://stackoverflow.com/question= s/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 stuf= f.

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,
=C2=A0 =C2=A0Oliver





--
Caml-list mailing list. =C2=A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners<= /a>
Bug reports: http://caml.inria.fr/bin/caml-bugs



--
= Bart: Look at me, I'm a grad student, I'm 30 years old and I made $= 600 dollars last year.
Marge: Bart! Don't make fun of grad students,= they just made a terrible life choice.
--047d7b339dbdf4f64804fec3f8f4--