package coq-vellvm

  1. Overview
  2. No Docs
Coq library implementing (executable) semantics for LLVM IR

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. S
    Steve Zdancewic <stevez@cis.upenn.edu>
  2. Y
    Yannick Zakowski <yannick.zakowski@inria.fr>
  3. C
    Calvin Beck <hobbes@seas.upenn.edu>
  4. I
    Irene Yoon <euisuny@cis.upenn.edu>
  5. G
    Gary (Hanxi) Chen <hanxic@seas.upenn.edu>

Maintainers

  1. S
    stevez@cis.upenn.edu

Sources

v1.0.20240627.tar.gz
sha256=8f1377ecc7f652004b6f98e0d4f4c3dd02ce53e4f840349e2191fa54d7089810

Description

Tags

date:2024-06-27 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm

Published: 28 Jun 2024

Dependencies (14)

  1. coq-quickchick >= "2.0.2" & < "2.0.3"
  2. coq-itree >= "5.1.2" & < "5.2~"
  3. coq-simple-io
  4. coq-mathcomp-ssreflect
  5. coq-flocq >= "4.1.1"
  6. coq-ceres
  7. coq-paco
  8. coq-ext-lib < "0.12.1"
  9. coq >= "8.19.0" & < "8.20~"
  10. qcheck
  11. menhir
  12. dune >= "2.8"
  13. cppo
  14. ocaml >= "4.14.0"

Dev Dependencies

None

Used by

None

Conflicts

None