This research project dedicated to formalizing and modeling application level services using dependent types theory and theorem proovers. This will cover KVS persistence, N2O protocol commutator and BPE business process engine a well known Synrc Erlang Applications.
The aim is to define mathematically clean applications, provide persistence of competational effects in KVS storage, proove some properties and invariants of the core.
- Maxim Sokhatsky