Re: [Caml-list] Program proof - how to do that?

[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É <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:
>>   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