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
erl2whyin the Erlang compiler
- Contact
- ---
- Links
- Core Erlang
The Why tool
erl2why