Name: Haskell FFI and Dependent Types in Agda
Start: 2015-03-24T17:45:00+10:00
End: 2015-03-24T20:45:00+10:00
Location: Red Hat

Haskell FFI Basics - Fraser Tweedale

Wanting to make use of libraries written in other langauges (often C) is a common situation in high-level languages, and Haskell is no exception. This talk will introduce and demonstrate real-world use of Haskell's C foreign function interface (FFI), including how to deal with some common C idioms. We will examine the c2hs tool which simplifies bindings and review some other Haskell FFI tools.

Attendees who are comfortable with Haskell syntax and have a passing familiarity with C (especially pointers) will get the most out of this presentation.

A dependently-typed Agda taster - Matt Brecknell

Let's tuck into some term-indexed types!

Part one

We'll see what it means to reify definitional equality of terms as a type, and how to use equality to rewrite types. We'll reinvent Sigma and Pi types, starting from the simple sums and products we all know and love.

Part two (next month)

We'll show how to build evidence that a certain thing can be found in a list, and how to use this evidence to safely retrieve a different thing from some other suitably-indexed heterogeneous list.

Finally, if we have time, we'll use what we just built to embed the simply-typed lambda calculus.

Ben Kolera

Katie

Nick Partridge

Brisbane Functional Programming Group (BFPG)

Technology

Functional Programming

Programming Languages

Scala

Haskell

Erlang Programming

Computer Programming

OCaml Programming

Haskell FFI and Dependent Types in Agda

Red Hat

Share

Brisbane Functional Programming Group (BFPG)

Haskell FFI and Dependent Types in Agda

Brisbane Functional Programming Group (BFPG)

Details

Members are also interested in