package coq-ott

  1. Overview
  2. No Docs
Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi

Install

Dune Dependency

www.cl.cam.ac.uk Edit opam file Versions (9)

Authors

  1. P
    Peter Sewell
  2. F
    Francesco Zappa Nardelli
  3. S
    Scott Owens

Maintainers

  1. P
    palmskog@gmail.com

Sources

0.31.tar.gz
sha512=d885ac3e7d835705342f476200bcbbdc278bcf44418d5365f02b4e92e4d630d6d080bfb008e6742fc3354de3379a99afc5263b66a612a9ac4ce20231f4500f4a

Description

Ott takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It can then generate a Coq version of the definition, which requires this library.

Tags

category:Computer Science/Semantics and Compilation/Semantics keyword:abstract syntax logpath:Ott date:2020-06-15

Published: 19 Nov 2020

Dependencies (1)

  1. coq >= "8.5" & < "8.12~"

Dev Dependencies

None

Used by (1)

  1. coq-mi-cho-coq

Conflicts (1)

  1. ott != version