hs-to-coq
Haskell to Coq converter
A tool that translates Haskell code to equivalent Coq code
Convert Haskell source code to Coq source code.
79 stars
13 watching
8 forks
Language: Coq
last commit: 6 months ago
Linked from 3 awesome lists
coqhaskell
aolofsson/awesome-opensource-hardware
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |
 serras/hinc | A Haskell code transpiler from another syntax to the standard Haskell syntax | 111 |
 kosmikus/lhs2tex | A tool for converting Haskell source code into LaTeX-compatible typesetting formats | 99 |
 thma/lambda-ski | Implementing a graph-reduction machine for a small functional language based on λ-calculus and combinatory logic | 28 |
 haskell/ghcup-hs | A tool for installing and managing the Glasgow Haskell Compiler (GHC) | 293 |
 sol/aeson-qq | A Haskell package that enables compile-time conversion of JSON strings to data structures using a custom quasiquoter. | 80 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
| plclub/metalib | A Coq-based metatheory library providing tools and examples for mechanizing programming language definitions and reasoning about them. | 73 |
 lpcic/coq-elpi | Provides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming | 141 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
 heinrichapfelmus/hyper-haskell | An interactive graphical interpreter for the Haskell programming language | 361 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |