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.34.tar.gz
sha512=371b59c0dc35207f8e85a939f03ae63fc654df50540ed5e656c5a40c5062ebfdfb1e02cfd499074f9d0b43afc165606b57dec4c96a4ca44ee91d1c1dcfa4deaf

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:2024-12-30

Published: 30 Dec 2024

Dependencies (1)

  1. coq >= "8.14" & < "8.21"

Dev Dependencies

None

Used by (1)

  1. coq-mi-cho-coq

Conflicts (1)

  1. ott != version