package coq-lemma-overloading

  1. Overview
  2. No Docs
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq

Install

Dune Dependency

github.com Edit opam file Versions (5)

Authors

  1. G
    Georges Gonthier
  2. B
    Beta Ziliani
  3. A
    Aleksandar Nanevski
  4. D
    Derek Dreyer

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.10.0.tar.gz
sha512=9da994cd10358f9c5b6e8bb3591819d23ff0def0f3b86ac585fa1eeb0a32f1a926e5066d279fbb84da173f8aa26c8e33bedb8a5260b40893f90467798eb2f92b

Description

This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.

Tags

category:Computer Science/Data Types and Data Structures keyword:canonical structures keyword:proof automation keyword:Hoare type theory keyword:lemma overloading logpath:LemmaOverloading date:2019-12-07

Published: 08 Dec 2019

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.7" & < "1.11~"
  2. coq >= "8.8" & < "8.12~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None