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.33.tar.gz
sha512=fd601ef958e52ca461eaff8175323416e3e524e1ba11fcf5328827ef2cb9ee3d54111843adb54d3c32e2f08c7c70214558bf5519fb8385bfa58049f22237c3c6

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:2023-01-16

Published: 18 Jan 2023

Dependencies (1)

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

Dev Dependencies

None

Used by (1)

  1. coq-mi-cho-coq

Conflicts (1)

  1. ott != version