Libx Awesomeリスト

    このページの内容

    Awesome Coq

    Coqを扱う資料や関連プロジェクトをまとめたAwesomeリストです。

    目次

    プロジェクト

    Framework

    • ConCert - 複数のSmart Contract言語へのCode Extraction Pipelineを備えたTest／検証Framework。
    • CoqEAL - 証明内のData Representation変更を容易にするFramework。
    • FCF - 暗号学的証明のFramework。
    • Fiat - Correct-by-Construction Programをほぼ自動合成。
    • FreeSpec - Effect／Effect Handlerを持つProgramをModularに検証するFramework。
    • Hoare Type Theory - Type Theoryとして定式化した逐次Separation LogicのShallow Embedding。
    • Hybrid - Object LogicのHigher-Order Abstract Syntax表現で推論するSystem。
    • Iris - Higher-Order Concurrent Separation Logic Framework。
    • Q*cert - Query Compilerを実装・検証するPlatform。
    • SSProve - Mathematical Components LibraryベースのModularな暗号学的証明Framework。
    • VCFloat - 浮動小数点計算を行うC Programの検証Framework。
    • Verdi - 分散System実装を形式検証するFramework。
    • VST - CompCert CompilerのClight言語に対して健全なHigher-Order Concurrent Impredicative Separation Logicで、Coq内のC Codeを検証するToolchain。

    User Interface

    • CoqIDE - Coqと対話するStandalone Graphical Tool。
    • Coqtail - Vim Text EditorベースのCoq Interface。
    • Coq LSP - 独自Document Checking Engineを持つVisual Studio Code／VSCodium向けLanguage Server／Extension。
    • Proof General - 拡張・CustomizableなEmacsベースのProof Assistant汎用Interface。
    • Company-Coq - Proof GeneralのCoq Mode向けIDE Extension。
    • opam-switch-mode - Menu／Commandからopam SwitchをLocal変更・ResetするProof General Extension。
    • jsCoq - BrowserでCoq Projectを実行できるJavaScript移植版。
    • Jupyter kernel for Coq - Jupyter Notebook Web環境のCoq対応。
    • VsCoq - Visual Studio Code／VSCodium向けLanguage Server／Extension。
    • VsCoq Legacy - Coq旧XML Protocolを使う後方互換Visual Studio Code／VSCodium Extension。
    • Waterproof editor - 対話型Notebookで数学証明を書く教育環境。
    • Tree Sitter Rocq - HelixなどのSyntax Highlightに有用な部分的Rocq Tree-Sitter Grammar。Rocq Codeの完全なParseには非推奨。

    Library

    • ALEA - Randomized Algorithmを推論するLibrary。
    • Algebra Tactics - Mathematical Components向けRing／Field Tactic。
    • Bignums - 任意精度数Library。
    • Bedrock Bit Vectors - 固定精度Machine Wordを推論するLibrary。
    • CertiGraph - Directed GraphとSeparation Logic内へのEmbeddingを推論。
    • CoLoR - Rewriting Theory、Lambda Calculus、TerminationのLibrary。Coq Standard Libraryを拡張する一般Data Structure Sub-Libraryを含みます。
    • coq-haskell - Haskell利用者のCoq移行を滑らかにするLibrary。
    • Coq-Kruskal - Rose TreeとKruskal Tree Theorem関連Library集。
    • CoqInterval - 実数式の不等式証明を行うTactic。
    • Coq record update - Coq Record Fieldを汎用的に更新するLibrary。
    • Coq-std++ - Coq向け拡張代替Standard Library。
    • ExtLib - ほかのCoq開発で有用なTheory／Plugin集。
    • FCSL-PCM - Pointer操作Programの検証で使うPartial Commutative Monoidの形式化。
    • Flocq - 浮動小数点数・計算の形式化。
    • Formalised Undecidable Problems - 決定不能問題とそれらのReductionのLibrary。
    • Hahn - ListとBinary Relationを推論するLibrary。
    • Interaction Trees - Recursive／Impure Programを表現するLibrary。
    • LibHyps - 証明内のHypothesisを管理・操作するLtac Tactic Library。
    • MathComp Extra - AKS Primality Test、RSA暗号化・復号などMathematical Components追加資料。
    • Mczify - Mathematical Componentsの数定義でMicromega Arithmetic Solverを利用可能にするLibrary。
    • Metalib - Locally Nameless Variable Binding表現を使うProgramming Language Metatheory Library。
    • Paco - Parameterized Coinduction Library。
    • Regular Language Representations - Regular Expression／Automataを含むRegular Languageの各定義間の変換。
    • Relation Algebra - Heterogeneous Binary RelationをModelとするAlgebraのModular形式化。
    • Simple IO - 利用者定義Primitive Operationを持つI/O Monad。
    • TLC - Coq Standard LibraryのNon-Constructive代替。

    Package／Build管理

    • coq_makefile - Coq同梱でMakefile生成ベースのBuild Tool。
    • Coq Nix Toolbox - CoqのLocal Build／CIを自動化するNix Helper Script。
    • Coq Package Index - opamベースのCoq Package集。
    • Coq Platform - 産業、教育、研究でのCoq利用を支えるPackage選集。
    • coq-community Templates - Coq Project設定File生成Template。
    • Debian Coq packages - Debian Testing Distributionで利用可能なCoq関連Package。
    • Docker-Coq - 多数のCoq Version向けDocker Image。
    • Docker-MathComp - Coq／Mathematical Componentsの多数のVersion組み合わせ向けDocker Image。
    • Docker-Coq GitHub Action - Docker-Coq／Docker-MathCompで使えるGitHub Container Action。
    • Dune - OCaml／Coq向けComposableでOpinionatedなBuild System（旧jbuilder）。
    • Nix - Atomic Upgrade／Rollback対応のLinuxなどUnix System向けPackage Manager。
    • Nix Coq packages - Nix向けCoq関連Package集。
    • opam - Multiple Compiler対応で柔軟かつGit-FriendlyなOCaml／Coq Package Manager。

    Plugin

    • AAC Tactics - 一部OperatorのAssociativity／Commutativityを法としてUniversally Quantified Equationを書き換えるTactic。
    • Coinduction - 強化Coinductionによる証明Plugin。
    • Coq-Elpi - Command／Tactic実装の広範なAPIを提供するλPrologベースExtension Framework。
    • CoqHammer - 過去の証明学習、Automated Proverへの問題変換、発見した証明の再構成を組み合わせる汎用Automated Reasoning Hammer Tool。
    • Equations - Coq向け関数定義Package。
    • Gappa - 浮動小数点Arithmetic／Round-Off ErrorのGoalを解くTactic。
    • Hierarchy Builder - Packed ClassベースのCoq Hierarchy宣言Command集。
    • Itauto - Function Symbol、Constructor、Arithmeticの命題推論を組み合わせるSMT風Tactic。
    • Ltac2 - 古典的Ltacに似た実験的Typed Tactic Language。
    • MetaCoq - CoqをCoqで形式化し、Coq Term操作／Certified Plugin開発Toolを提供するProject。
    • Mtac2 - Backward Reasoning向けTyped Tacticを追加するPlugin。
    • Paramcoq - Coq TermのParametricity Translationを生成。
    • QuickChick - Randomized Property-Based Testing Plugin。
    • SMTCoq - 外部SAT／SMT Solver由来Proof Witnessを検査するTool。
    • Tactician - 導入済みCoq Package全体のTactic Scriptから学び、次に実行するTacticを提案、またはProof Synthesisを完全自動化する対話型Tool。
    • Unicoq - 既存Unification Algorithmを強化版へ置換するPlugin。
    • Waterproof proof language - 非機械的な数学証明に似たStyleでProof Scriptを書くLanguageを提供。

    Puzzle／Game

    • Coqoban - 日本の倉庫番GameのCoq実装。
    • Hanoi - 一般化とConfiguration定理を含むCoqのTower of Hanoi。
    • Mini-Rubik - 2x2x2 Rubik’s CubeのCoq形式化／Solver。
    • Name the Biggest Number - Coqで最大数の称号を証明した候補を投稿するRepository。
    • Natural Number Game - Lean Prover向けNatural Number GameのCoq版。
    • Sudoku - Sudoku Number-Placement PuzzleのCoq形式化／Solver。
    • T2048 - 2048 Sliding Tile GameのCoq版。

    Tool

    • Alectryon - Coq Codeと文章を組み合わせた技術文書を書くTool集。
    • Autosubst-ocaml - Renaming／SubstitutionなどSyntax内Binder処理用Coq Code生成Tool。
    • CFML - Separation LogicでOCaml ProgramのPropertyを証明。
    • coq2html - Coq向け代替HTML Documentation Generator。
    • coqdoc - Coq CodeからLaTeX／HTML Fileを生成する標準Documentation Tool。
    • CoqOfOCaml - OCaml CodeからIdiomaticなCoqを生成。
    • coq-dpdgraph - Coq Object間Dependency Graphを構築。
    • coq-scripts - Proof時間集計などCoq File処理Script。
    • coq-tools - Coq Development操作Script。
      • find-bug.py - Errorを生むSource Fileを自動最小化し、Coq Bugの小さなTest Caseを作成。
      • absolutize-imports.py - File Name Shadowingに対しDependency読込を堅牢化。
      • inline-imports.py - 全Dependency読込をInline化し、DevelopmentからStandalone Source Fileを作成。
      • minimize-requires.py - 未使用Dependencyの読込を除去。
      • move-requires.py - 全Dependency読込文をSource File先頭へ移動。
      • move-vernaculars.py - 多数のVernacular Command／Inner LemmaをProof Script Block外へ移動。
      • proof-using-helper.py - Source FileへProof Annotationを追加し、Parallel Provingを高速化。
    • Cosette - SQL Query Equivalenceを推論するAutomated Solver。
    • hs-to-coq - Haskell Codeから等価なCoq CodeへのConverter。
    • lngen - Locally Nameless Coq定義／証明生成Tool。
    • Menhir - Verified Parser向けCoq Codeを出力できるParser Generator。
    • mCoq - Coq Project向けMutation Analysis Tool。
    • Ott - Coqへ変換できるProgramming Language／Calculus定義記述Tool。
    • PyCoq - Python 3内からCoqと対話するBinding／Library集。
    • Rocqnavi - Index、ClickableなNotation、Comment内Markdown／LaTeX Formatなどを追加したcoq2html Fork。
    • Roosterize - Coq ProjectのLemma名提案Tool。
    • Sail - Processor ISA Semanticsを指定しCoq定義を生成。
    • SerAPI - Coq CodeとJSON／S-Expression間をSerialize／DeserializeするTool／OCaml Library。
    • Trakt - Proof Automation Tactic向け汎用Goal Preprocessing Tool。

    型理論と数学

    • Analysis - Mathematical Components互換のClassical Real Analysis Library。
    • Category Theory in Coq - Category TheoryのAxiom-Free形式化。
    • Completeness and Decidability of Modal Logic Calculi - Logic K、K*、CTL、PDLのSoundness、Completeness、Decidability。
    • CoqPrime - Pocklington／Elliptic Curve CertificateによるPrimality認定Library。
    • CoRN - Constructive Real Analysis／Algebra Library。
    • Coqtail Math - ArithmeticからReal／Complex Analysisまでの数学結果Library。
    • Coquelicot - Standard Library互換でUsabilityを重視するClassical Real Analysis形式化。
    • Finmap - Finite Map、Set、MultisetによるMathematical Components拡張。
    • Four Color Theorem - Graph Theoryの画期的成果Four Color TheoremのFormal Proof。
    • Gaia - Set Theory／Number Theoryを含むBourbaki「Elements of Mathematics」の実装。
    • GeoCoq - Tarski Axiom SystemベースのGeometry形式化。
    • Graph Theory - Graph Theory結果の形式化。
    • Homotopy Type Theory - Homotopy-Theoretic Ideaの開発。
    • Infotheo - Information Theory／Linear Error-Correcting Codeの形式化。
    • Mathematical Components - とりわけGroup Theoryに注力する数学Theory形式化。
    • Math Classes - Type Classベースの数学Structure抽象Interface。
    • Monae - Monadic Effect／Equational Reasoning。
    • Odd Order Theorem - Finite Group Theoryの画期的成果Odd Order TheoremのFormal Proof。
    • Puiseuxth - Puiseux’s Theoremの証明とPuiseux Series多項式Rootの計算。
    • UniMath - Univalentな視点で大規模な数学体系を形式化するLibrary。

    検証済みSoftware

    • CompCert - ほぼ全C言語（ISO C99）向けHigh-Assurance Compiler。PowerPC、ARM、RISC-V、x86の効率的Codeを生成。
    • Ceramist - Bloom Filterなど検証済みHash-Based Approximate Membership Structure。
    • CertiCoq - Coq内部言語GallinaからCompCert ClightへのVerified Compiler。
    • Fiat-Crypto - Cryptographic Primitive Code生成。
    • Functional Algorithms Verified in SSReflect - Search、Sortなど基本問題のPurely Functionalな検証済み実装。
    • Incremental Cycles - GraphのIncremental Cycle Detection Algorithmの検証済みOCaml実装。
    • Jasmin - High-Assurance／High-Speed Cryptography向け形式化言語／Verified Compiler。
    • JSCert - Verified Reference Interpreterを持つECMAScript 5（JavaScript）のCoq仕様。
    • lambda-rust - Rust Core Language／Type SystemのFormal Model、Type SystemのLogical Relation、一部Rust LibraryのSafety Proof。
    • Prosa - Real-Time System Schedulability Analysisの定義・証明。
    • RISC-V Specification in Coq - RISC-V Processor ISA／Extensionの定義。
    • Stable sort algorithms in Coq - Merge Sort関数のStabilityを含む汎用・ModularなCorrectness Proof。
    • Tarjan and Kosaraju - Finite GraphのTopological Sort／Strongly Connected Component探索Algorithmの検証済み実装。
    • Vélus - Lustre/Scade風Dataflow Synchronous Language向けVerified Compiler。
    • Verdi Raft - Verdi FrameworkでCoq検証されたRaft Distributed Consensus Protocol実装。
    • WasmCert-Coq - WebAssembly（Wasm）1.0仕様のCoq形式化。

    資料

    Community

    Blog

    書籍

    講義資料

    Tutorial／Hint