Next meeting on Wednesday May 22nd

[Erik de Castro Lopo]

Hi all,

The next meeting will be help on Wednesday May 22nd.

This month we have two talks:

Tim McGilchrist : TBA

Mark Hopkins : Dependent Types Made Difficult

Abstracts below.

The RSVP is here:

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

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,
Erik

Dependent Types Made Difficult
------------------------------
The field of categorical semantics shows that the simply typed lambda
calculus has a natural interpretation in any Cartesian closed category: it
is their "internal language".

In "Compiling to Categories" Conal Elliott put this correspondence to work
in the form of a GHC plugin, yielding applications including hardware
circuits, automatic differentiation, incremental compilation and interval
analysis.

Lately I've been trying to understand: what is the categorical semantics of
*dependent types*? I'll look at perhaps the simplest answer to this
question - dependent type theory is the internal language of so-called
"locally Cartesian closed categories". I'll explore (with pictures!) how
dependent sum and product functors, which model dependent sum and product
types, arise in the category of sets.

--
----------------------------------------------------------------------
Erik de Castro Lopo
http://www.mega-nerd.com/

[Erik de Castro Lopo]

Erik de Castro Lopo wrote:

> This month we have two talks:
>
> Tim McGilchrist : TBA
>
> Mark Hopkins : Dependent Types Made Difficult

There has been a very slight change of plan to the above schedule,
namely that I will be presenting instead of Tim. Abstract below.

Cheers,
Erik

Recent Developments at IOHK
---------------------------
In this presentation I will discuss two techniques that we are
using at IOHK to improve the quality and level of confidence in
our Haskell code. Those two tehcniques are "Semi Formal Methods"
and the use of dependently typed network protocols.