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.11.0.tar.gz
sha512=58df76ccd7a76da1ca5460d6fc6f8a99fa7f450678098fa45c2e2b92c2cb658586b9abd6c0e3c56177578a28343c287b232ebc07448078f2a218c37db130b3d7

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:2020-02-01

Published: 01 Feb 2020

Dependencies

None

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "1.7" & < "1.12~") | (= "dev")
  2. coq (>= "8.10" & < "8.12~") | (= "dev")

Used by

None

Conflicts

None