This project aims to investigate and compare different big-step style formal semantics and their usability, executability. We use a small Core Erlang-like functional language for this purpose. The structure of the files is the following:
CE_Syntax.vcontains the syntax and semantic domain for the languageCE_Helpers.vcontains helper functions and lemmas about the syntaxCE_Env.vcontains the definition of environments and the correcponding functionsCE_Aux.vcontains the definition of auxiliary functions which are used when evaluatingECallexpressionsCE_NOS.vcontains the traditional inductive big-step semanticsCE_PBOS.vcontains the pretty-big-step semanticsCE_FBOS.vcontains the functional big-step semanticsCE_Tests.vcontains simple expression evaluation testsCE_Equivs.vcontains expression equivalence proofs, moreover, theorems about the functional big-step semantics, and semantics equivalence
The source code is licensed under GPL v3.
Supported by the project "Integrált kutatói utánpótlás-képzési program az informatika és számítástudomány diszciplináris területein (Integrated program for training new generation of researchers in the disciplinary fields of computer science)", No. EFOP-3.6.3-VEKOP-16-2017-00002. The project has been supported by the European Union and co-funded by the European Social Fund.