Name: Hands-on F*: Dependent Types, Effects and the Future of Functional Programming
Start: 2016-04-26T18:00:00+02:00
End: 2016-04-26T21:00:00+02:00
Location: Prosa (ADA lokale)

UPDATE: There will be two initial talks, one from Ahmad and another one from Alessandro, both F* related, and then we will have some hands-on.

---

Type systems are awesome! They allow you to get great editor support, they provide high-level documentation for your functions absolutely free, and they help you to avoid silly mistakes like dividing a integer with a string. Modern languages with more advanced type systems allow you to go beyond finding silly mistakes, to help you to avoid more complex errors like writing to a readonly file, and showing that your sorting algorithm truly produces a sorted list. F* is a modern F#-like language which supports an automated refinement-types based system, that provides the aforementioned features in a user-friendly way. Not only is F* good for reasoning about pure programs, but also supports a sophisticated effect system that allows not just writing fully fledged F#-style programs---with heap references, exceptions and IO---but also effectively reason about these things. Since F* can compile to popular languages like F# and OCaml, it can be used together with existing code bases, and it has already been used by the language implementers to provide verified implementations of TLS-1.2 and even a smaller version of F* itself!

I intend to provide a short casual introduction to F* which highlights the core ideas behind the language. Then afterwards I hope there can be a small hack-a-long where where some of us pick a couple of smaller F* programs from the topic list ( https://github.com/FStarLang/FStar/wiki/Project-topics-on-F *) to code on together, and others have the opportunity to take the tutorial ( https://www.fstar-lang.org/tutorial/ ) and have a smaller discussion about it.

About Ahmad Salim Al-Sibahi:
I am a PhD student at the IT University of Copenhagen working on developing foundational techniques and prototype tools for verification of transformation languages. I have had some experience with generic programming in dependently-typed languages, and have contributed a little to the Idris programming language.

---

F* can be used to verify many useful properties of programs. One major application of software verification is security: dependent types allow to express security properties such as the secrecy and authenticity of communication. In this part of the presentation we'll explore how this can be done in F*.

About Alessandro Bruni:
I am a postdoc researcher at the IT university of Copenhagen working on the verification of security protocols by means of automated reasoning. He previously worked on the verification of security protocols for automotive, finding and fixing flaws in existing designs.

---

The ADA meeting room fits about 25 people and if we need more space, we can use the canteen, which has a capacity of +50.

Regards,

Ramón and Joakim

Ramón Soto Mathiesen

Joakim Ahnfelt-Rønne

Mødegruppe for F#unktionelle Københavnere

Technology

Computer Programming

Erlang Programming

Clojure

Functional Programming

Haskell

Scala

Web Development

New Technology

Lisp

Programming Languages

Software Development

Open Source

F# Programming

OCaml Programming

Hands-on F*: Dependent Types, Effects and the Future of Functional Programming

Prosa (ADA lokale)

Share

Mødegruppe for F#unktionelle Københavnere

Hands-on F*: Dependent Types, Effects and the Future of Functional Programming

Mødegruppe for F#unktionelle Københavnere

Details

UPDATE: There will be two initial talks, one from Ahmad and another one from Alessandro, both F* related, and then we will have some hands-on.

Members are also interested in