jwiegley / Coq Haskell
Licence: other
A library for formalizing Haskell types and functions in Coq
Projects that are alternatives of or similar to Coq Haskell
FourcolorFormal proof of the Four Color Theorem
Stars: ✭ 87 (-35.56%)
Mutual labels: coq
ErgoThe Language for Smart Legal Contracts
Stars: ✭ 108 (-20%)
Mutual labels: coq
GeocoqA formalization of geometry in Coq based on Tarski's axiom system
Stars: ✭ 128 (-5.19%)
Mutual labels: coq
TtliteA SuperCompiler for Martin-Löf's Type Theory
Stars: ✭ 94 (-30.37%)
Mutual labels: coq
Mindless CodingMindless, verified (erasably) coding using dependent types
Stars: ✭ 104 (-22.96%)
Mutual labels: coq
Awesome ProvableA curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-17.78%)
Mutual labels: coq
TypetheoryThe mathematical study of type theories, in univalent foundations
Stars: ✭ 86 (-36.3%)
Mutual labels: coq
Math ClassesA library of abstract interfaces for mathematical structures in Coq [[email protected]]
Stars: ✭ 133 (-1.48%)
Mutual labels: coq
CeramistVerified hash-based AMQ structures in Coq
Stars: ✭ 107 (-20.74%)
Mutual labels: coq
FiatMostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-11.85%)
Mutual labels: coq
PeacoqPeaCoq is a pretty Coq, isn't it?
Stars: ✭ 99 (-26.67%)
Mutual labels: coq
Coq Ext LibA library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Stars: ✭ 102 (-24.44%)
Mutual labels: coq
IronCoq formalizations of functional languages.
Stars: ✭ 114 (-15.56%)
Mutual labels: coq
Coq SerapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
Stars: ✭ 87 (-35.56%)
Mutual labels: coq
Dotformalization of the Dependent Object Types (DOT) calculus
Stars: ✭ 132 (-2.22%)
Mutual labels: coq
VscoqCoq Support for Visual Studio Code
Stars: ✭ 85 (-37.04%)
Mutual labels: coq
CoqtailInteractive Coq Proofs in Vim
Stars: ✭ 109 (-19.26%)
Mutual labels: coq
ProofsA selection of formal proofs in Coq.
Stars: ✭ 135 (+0%)
Mutual labels: coq
InteractiontreesA Library for Representing Recursive and Impure Programs in Coq
Stars: ✭ 133 (-1.48%)
Mutual labels: coq
Coq Of OcamlImport OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-13.33%)
Mutual labels: coq
coq-haskell
This library is designed for Haskell users who are either using Coq to build
code intended for extraction to Haskell, or who wish to prototype/prove their
algorithms in Coq. It provides a collection of definitions and notations to
make Gallina more familiar to Haskellers.
It is based on the ssreflect library, and avoids most uses of the Coq standard
library (except for the StronglySorted
type). Wherever possible, Haskell
named functions and types are simply aliases for their Coq equivalents, to
facilitate interaction with other Coq users. This means, for example, that one
should use a + b
with constructors named inl
and inr
.
Thus, the aim is not to make Coq look exactly like Haskell, but only to smooth
the divide.
This library also allows the use of Haskell Monads within Coq developments,
with one caveat: In order to satisfy the extraction machinery, entry-points on
the Coq side (as well as calls back) must use Yoneda m a
rather than simply
m a
, since the latter fully erases the a
type.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at
[email protected].