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.29.tar.gz
sha512=2ffc10e5d6290b5a737add419e5441b85a60fda7a9c4544f91bcfd8cd69e318d465787b2500003109186cc3945c3dcb5661371a419c3ef117adff9fc2d8f3e5b

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:2019-08-01

Published: 03 Aug 2019

Dependencies (1)

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

Dev Dependencies

None

Used by (1)

  1. coq-mi-cho-coq

Conflicts

None