FP /

Core Erlang to Why Backend

1 Background

Core Erlang is an intermediate representation of Erlang. In comparison with Erlang, it has simpler semantics and more regular structures. Core Erlang is designed to make it easier to develop tools for analysing code

Why is a verification condition generator (VCG) for a small intermediate verification language with annotations, which enable property specification, and type safety, through simple type checking. Part of the erl2why is a support library for representing Erlang structures in Why, which can be used in the translation of Erlang programs to the why Language.

2 Goal

To implement a translation from Core Erlang to Why and integrate it in erl2why.

3 Work plan

  • Study the Core Erlang language
  • Study the current translation from Erlang to Why in erl2why
  • Implement a new translation from Core Erlang to Why for erl2why
  • Explore how to integrate erl2why in the Erlang compiler
Core Erlang
The Why tool