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
15 stars
2 watching
8 forks
Language: Prolog
last commit: almost 2 years agoLinked 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. | 220 |
 andrew-johnson-4/lsts | A programming language and proof assistant built on top of Rust. | 114 |
 cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
 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 | A proof assistant based on a type theory for synthetic ∞-categories. | 212 |
 marklogic/ml-gradle | Automates tasks involving MarkLogic using Gradle | 72 |
 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 | 159 |
| 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 | 191 |
 ahgamut/janet | A dynamic language with user scripting capabilities to extend C/C++ programs and automate system tasks. | 5 |
 mtac2/mtac2 | A plugin for Coq that extends its proof assistant with a typed tactic language for backward reasoning. | 51 |