A formal semantics for SPARK in Coq

This page describes the current state of the spark semantics in Coq. This owrk started during the internship of Zhi Zhang from SAntoS lab (Kansas University) in the CPR team of CEDRIC lab during summer 2013.

Anonymous access to the development archive:

git clone --recursive https://forge.open-do.org/anonscm/git/spark2014/spark2014.git

directory: language_formal/spark2014_semantics

Current Status

Zhi developed the semantics of the following subset of the targeted language (itself a subset of spark 2014):

In short, annotation were not planned for Zhi internship, and procedure bodies and calls was a too big piece of formalization for such a short period of time. We knew that from the beginning.

The whole formalization is clean and is clearly a very good starting point to achieve the formalization of the subset. We defined two semantics:

This work has been presented as an industrial paper at ACM HILT2013 conference.