Skip to main content

Semantics

The Gospel paper1 describes how the semantics of the Gospel language is defined by its translation to separation logic.

The gospel tool does only some type-checking of your Gospel-specified modules. To exploit the semantics of your specifications, you'll have to use one of the various tools.

  1. Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira. GOSPEL -Providing OCaml with a Formal Specification Language. FM 2019 - 23rd International Symposium on Formal Methods, Oct 2019, Porto, Portugal. ⟨hal-02157484⟩↩