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.32.tar.gz
sha512=f38e12c079426c5a460a9ab24e58f098410ceb5ae0284c1719c50f6d7cd88f6b9c4da6beb5425c03f2dc056c7a9cb597f9bf2983abb525e3c003e45858496ad3

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:2022-03-09

Published: 23 May 2022

Dependencies (1)

  1. coq >= "8.6"

Dev Dependencies

None

Used by (1)

  1. coq-mi-cho-coq

Conflicts (1)

  1. ott != version