Formal semantics for a model of Opal (https://capra.cs.cornell.edu/research/opal/)
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
lib/cpdtlib
src
.gitignore
Makefile
Makefile.tex
README.md
_CoqProject
revision.tex
semantics.pdf
semantics.tex

README.md

Opal Semantics

Alex Renda, Harrison Goldstein, Sarah Bird, Chris Quirk, Adrian Sampson

Contents

  1. Formalization of Opal semantics (semantics.pdf).
  2. Coq implementation of semantics (src/OpalSemantics.v)
  3. Coq implementation of an interpreter (src/OpalInterp.v)
  4. Theorems and proofs over the Coq implementation of semantics (src/OpalProofs.v)
  5. An unverified "compiler" from a nicer syntax to constructors for the Coq embedding (src/compiler)

Usage

Run make to make everything, make tex to regenerate the semantics pdf, and make coq to machine check each of the proofs.