Next meeting on Wednesday October 23rd

[Ben Lippmeier]

Hi all,

The next meeting will be held on Wednesday October 23rd.

This month we have one talk lined up so far, and one slot still free.

If you have something to talk about then please reply to this message.

   Ben Lippmeier: The Why3 theorem proving framework.

Abstract below.

The RSVP is here:

   https://www.meetup.com/FP-Syd/events/vcqlmpyznbfc/

Doors open at 6pm, meeting proper starts at 6:30.

Everybody who intends to show up on the night shoud RSVP ASAP to allow our
hosts Atlassian to sort out the catering. People who said they were
going but now find that they can't should likewise update their status.

Cheers,
Ben

The Why3 theorem proving framework

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The Why3 framework provides a programming language WhyML and an IDE that connects to external SMT solvers (automatic theorem provers). WhyML is a dialect of ML that allows one to specify pre and post-conditions for functions, and to define logical theories. When a WhyML program is loaded into the IDE it generates verification conditions for each of the functions, which the user can send to an external solver to verify. In the happy case the solver says your thing is true and your function has no bugs. In the not-so-happy case you can use Why3’s builtin tactics to figure out why either 1) the solver isn’t smart enough to know your thing is true, or 2) your thing was never true to begin with. In the unhappy case the verification condition can be exported to an interactive theorem prover like Coq for manual avian attention. I’ve spent about 4 weeks full time working directly with Why3 and found it quite usable, with only a few rough edges. I’ve managed to formalise some of the key operators provided in a TensorFlow like language, such as max-pool and multidimensional array slicing.

[Ben Lippmeier]

> On 20 Oct 2019, at 3:51 pm, Ben Lippmeier <be...@ouroborus.net> wrote:
>
> This month we have one talk lined up so far, and one slot still free.
> If you have something to talk about then please reply to this message.

Note that talks don’t need to be lecture style presentations. Show-and-tells, paper summaries, and 10 minute rants are also quite acceptable.

Ben.

[Suzanne Duggan]

hi 

How do I unsubscribe from this?

thanks

--
You received this message because you are subscribed to the Google Groups "fp-syd" group.
To unsubscribe from this group and stop receiving emails from it, send an email to fp-syd+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/fp-syd/00D9A3D2-BB0C-4D91-A715-0A1E77A8D4AA%40ouroborus.net.

[Ben Lippmeier]

On 20 Oct 2019, at 11:38 pm, Rongmin Lu <rongm...@gmail.com> wrote:

If nobody else has taken the slot, and paper summaries are fine, I'd like to talk about a couple of new papers on automatic differentiation. The proposed title is "Differentiating curry", and I'd probably be talking about the following preprints (this is a preliminary list and may change as I draft the talk):

https://openreview.net/forum?id=ryxuz9SzDB (The inspiration for the title :))

https://arxiv.org/abs/1910.07065

Ok, great. I’ll update the meetup page.

Ben.