trakt
Proof automation tool
Automates goal preprocessing in proof automation tactics using a custom-built tool
A generic goal preprocessing tool for proof automation tactics in Coq
14 stars
2 watching
7 forks
Language: Prolog
last commit: about 1 month ago
Linked from 1 awesome list
coq-community/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 218 |
 andrew-johnson-4/lsts | A programming language and proof assistant built around type theory and lambda calculus. | 114 |
 cpitclaudel/alectryon | Tools for processing Coq code and prose in technical documents | 236 |
 phorward/rapidbatch | A scripting language platform designed to automate tasks and processes. | 10 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 rzk-lang/rzk | An experimental proof assistant built on top of a type theory for synthetic ∞-categories. | 205 |
 marklogic/ml-gradle | Automates tasks involving MarkLogic using Gradle | 73 |
 xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
 fluidex/plonkit | Provides tools and utilities for generating and verifying proofs in a zkSNARK proof system | 158 |
| xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 ahgamut/janet | A dynamic language with user scripting capabilities to extend C/C++ programs and automate system tasks. | 5 |
 mtac2/mtac2 | A plugin for the Coq proof assistant that enables typed tactic language and supports advanced tactics | 51 |