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É (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 > > > > > > -- > 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 > -- 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.