Typed State Machine: A Dream of Humankind

Making State Machines safe, composable, and practical using types – the author of Idris has boldly taken on the dream of humankind, and achieved it through an abstraction called Control.ST library (http://docs.idris-lang.org/en/latest/st/).

In this session, I will show what Control.ST is, and how it can be used. Even though it was originally written in Idris with dependent types, we will also look into how far we can take Scala to mimic it. See also ‘State Machines All The Way Down’ paper (https://www.idris-lang.org/drafts/sms.pdf).

Session length

40 minutes

Language of the presentation

Japanese

Target audience

Intermediate: Requires a basic knowledge of the area

Who is your session intended to

People who like types, and people interested in dependent types.

Speaker

osiire