ABS Metatheory

Formal metatheory in Coq for the ABS language.

Meta

• Author(s):
  • Åsmund Kløvstad
  • Karl Palmskog
• License: MIT License
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • Ott Coq library 0.33 or later
  • Equations Coq library 1.3 or later
  • Coq-Std++ 1.9.0 or later
• Coq namespace: ABS
• Related publication(s):
  • ABS: A Core Language for Abstract Behavioral Specification doi:10.1007/978-3-642-25271-6_8

Building instructions

To install all dependencies, do:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.18.0 coq-ott coq-equations coq-stdpp

To build when dependencies are installed, do:

git clone https://github.com/kth-step/abs-metatheory.git
cd abs-metatheory
make   # or make -j <number-of-cores-on-your-machine> 

To build a pdf documenting the project, ensure that ott and TeX Live (pdflatex) are installed, and do:

make docs/report/main.pdf

Note that the source file to edit for this pdf is docs/report/main.mng.

Documentation

• latest technical report
• latest coqdoc documentation

See also ABS Tools.