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.9.0.tar.gz
sha256=7e57155182bac6e9940e2d0c509da702f600c2898efb2e65edad367c9515210d

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-05-15

Published: 16 May 2019

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.7.0" & < "1.9~"
  2. coq >= "8.8" & < "8.10~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None