Introduction to a type system: session types

Correctness in software development is an important subject that has been explored by the academy and by the industry. How to ensure that your program cannot fail? How to ensure that what you're developing will work as expected without unwanted side-effects? etc.

Since then, several approaches were developed; one of them is static type analysis, a methodology which tries to prove that your program is correct based on the mathematical types theory, whose basic assumption is that unless your program can prove it attends its basic contracts, it is faulty. Considering Erlang is widely known by its focus on fault-tolerance and, by consequence, guarantees of reliability, there have been several attempts to improve Erlang programs by proving their correctness with type systems but such attempts have failed.

This talk proposes to explain what is a type system, why attempts to type strictly Erlang have failed and how the theory of Session Types might prove to be a way to achieve correctness in environments like Erlang's.

OBJECTIVES

 

• Present the concept of static type analysis
• Present the research so far in session types applied to programming
• Build hype over the future of environments based on the actor-message model

 

TARGET AUDIENCE

Developers who have before had to handle bugs in their code; functional programming enthusiasts.