{"payload":{"pageCount":2,"repositories":[{"type":"Public","name":"coq-performance-tests","owner":"coq-community","isFork":false,"description":"A library of Coq source files testing for performance regressions on Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/JasonGross/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/JasonGross\">@JasonGross</a>]","allTopics":["testing","performance","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":2,"issueCount":1,"starsCount":6,"forksCount":5,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-06-01T04:07:18.937Z"}},{"type":"Public","name":"coq-ext-lib","owner":"coq-community","isFork":false,"description":"A library of Coq definitions, theorems, and tactics. [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/gmalecha/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/gmalecha\">@gmalecha</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/liyishuai/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/liyishuai\">@liyishuai</a>] ","allTopics":["library","programming","coq","coq-ci","coq-platform"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":16,"starsCount":123,"forksCount":45,"license":"BSD 2-Clause \"Simplified\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-20T07:15:57.216Z"}},{"type":"Public","name":"paramcoq","owner":"coq-community","isFork":false,"description":"Coq plugin for parametricity [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/proux01/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/proux01\">@proux01</a>]","allTopics":["coq-plugin","parametricity","docker-coq-action","coq-ci","coq-platform","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":6,"starsCount":44,"forksCount":22,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-13T13:11:33.921Z"}},{"type":"Public","name":"fourcolor","owner":"coq-community","isFork":false,"description":"Formal proof of the Four Color Theorem [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/ybertot/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/ybertot\">@ybertot</a>]","allTopics":["ssreflect","four-color-theorem","mathcomp","coq-ci","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":2,"issueCount":0,"starsCount":152,"forksCount":19,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-29T07:58:09.829Z"}},{"type":"Public","name":"trocq","owner":"coq-community","isFork":false,"description":"A modular parametricity plugin for proof transfer in Coq [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/CohenCyril/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/CohenCyril\">@CohenCyril</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/ecranceMERCE/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/ecranceMERCE\">@ecranceMERCE</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/amahboubi/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/amahboubi\">@amahboubi</a>]","allTopics":["coq","parametricity"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":4,"issueCount":14,"starsCount":15,"forksCount":1,"license":"GNU Lesser General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-27T11:18:03.948Z"}},{"type":"Public","name":"stalmarck","owner":"coq-community","isFork":false,"description":"Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["coq","tautology","coq-plugin","tautology-checking","coq-extraction","docker-coq-action","nix-action","coq-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":3,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-23T17:16:54.384Z"}},{"type":"Public","name":"atbr","owner":"coq-community","isFork":false,"description":"Coq library and tactic for deciding Kleene algebras [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/tchajed/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/tchajed\">@tchajed</a>]","allTopics":["coq","coq-tactic","kleene-algebra","coq-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":23,"forksCount":5,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-23T17:13:59.948Z"}},{"type":"Public","name":"math-classes","owner":"coq-community","isFork":false,"description":"A library of abstract interfaces for mathematical structures in Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/spitters/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/spitters\">@spitters</a>]","allTopics":["mathematics","typeclasses","coq-library","coq-ci","coq-platform","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":9,"starsCount":158,"forksCount":42,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-23T12:55:10.828Z"}},{"type":"Public","name":"corn","owner":"coq-community","isFork":false,"description":"Coq Repository at Nijmegen [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/spitters/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/spitters\">@spitters</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/VincentSe/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/VincentSe\">@VincentSe</a>]","allTopics":["coq-library","real-number","coq-ci","coq-platform","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":8,"starsCount":108,"forksCount":43,"license":"GNU General Public License v2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-23T14:20:07.671Z"}},{"type":"Public","name":"bignums","owner":"coq-community","isFork":false,"description":"Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/proux01/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/proux01\">@proux01</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/erikmd/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/erikmd\">@erikmd</a>]","allTopics":["large-numbers","coq-plugin","docker-coq-action","coq-ci","coq-platform","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":1,"starsCount":22,"forksCount":21,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-16T07:37:35.271Z"}},{"type":"Public","name":"coqeal","owner":"coq-community","isFork":false,"description":"The Coq Effective Algebra Library [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/CohenCyril/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/CohenCyril\">@CohenCyril</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/proux01/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/proux01\">@proux01</a>]","allTopics":["coq","refinement","mathcomp","coq-ci","coq-platform","mathcomp-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":3,"issueCount":5,"starsCount":64,"forksCount":15,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-29T14:12:41.783Z"}},{"type":"Public","name":"bits","owner":"coq-community","isFork":false,"description":"A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/anton-trunov/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/anton-trunov\">@anton-trunov</a>]","allTopics":["bitset","coq-library","ssreflect","paper-artifacts","coq-extraction","coq","mathcomp"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":3,"starsCount":22,"forksCount":5,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-28T16:41:16.888Z"}},{"type":"Public","name":"coq-dpdgraph","owner":"coq-community","isFork":false,"description":"Build dependency graphs between Coq objects [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/Karmaki/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/Karmaki\">@Karmaki</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/ybertot/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/ybertot\">@ybertot</a>]","allTopics":["dependency-analysis","dependency-graph","docker-coq-action","coq-ci","coq-platform","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":10,"issueCount":9,"starsCount":84,"forksCount":28,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-04T21:07:45.225Z"}},{"type":"Public","name":"apery","owner":"coq-community","isFork":false,"description":"A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/amahboubi/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/amahboubi\">@amahboubi</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/pi8027/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/pi8027\">@pi8027</a>]","allTopics":["ssreflect","mathcomp","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":4,"starsCount":19,"forksCount":5,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-20T22:12:30.080Z"}},{"type":"Public","name":"graph-theory","owner":"coq-community","isFork":false,"description":"Graph Theory [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/chdoc/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/chdoc\">@chdoc</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/damien-pous/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/damien-pous\">@damien-pous</a>]","allTopics":["coq","graph-theory","mathcomp","docker-coq-action","mathcomp-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":2,"starsCount":30,"forksCount":3,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-20T15:55:04.898Z"}},{"type":"Public","name":"hydra-battles","owner":"coq-community","isFork":false,"description":"Variations on Kirby &amp; Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/Casteran/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/Casteran\">@Casteran</a>]","allTopics":["discrete-mathematics","formal-proofs","primitive-recursive-functions","ordinal-notations","docker-coq-action","hydra-battles","coq-nix-toolbox","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":5,"issueCount":7,"starsCount":60,"forksCount":12,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-19T16:13:36.868Z"}},{"type":"Public","name":"notation-gallery","owner":"coq-community","isFork":false,"description":"Examples showing best practices for using Coq notations and custom entries [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/bcpierce00/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/bcpierce00\">@bcpierce00</a>]","allTopics":[],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":0,"starsCount":9,"forksCount":1,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-02T09:55:30.641Z"}},{"type":"Public","name":"reglang","owner":"coq-community","isFork":false,"description":"Regular Language Representations in Coq [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/chdoc/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/chdoc\">@chdoc</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["regexp","coq","regular-languages","ssreflect","mathcomp","docker-coq-action","coq-nix-toolbox","coq-platform","mathcomp-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":1,"starsCount":42,"forksCount":6,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-19T13:40:06.532Z"}},{"type":"Public","name":"coq-mmaps","owner":"coq-community","isFork":false,"description":"Modular Finite Maps over Ordered Types in Coq [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/letouzey/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/letouzey\">@letouzey</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["avl-tree","red-black-tree","docker-coq-action","finite-maps","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":1,"starsCount":8,"forksCount":3,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-08T15:22:04.002Z"}},{"type":"Public","name":"coqtail-math","owner":"coq-community","isFork":false,"description":"Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis. [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/jmadiot/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/jmadiot\">@jmadiot</a>]","allTopics":["real-analysis","coq","complex-analysis"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":0,"starsCount":15,"forksCount":0,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-06T22:14:19.234Z"}},{"type":"Public","name":"coq-art","owner":"coq-community","isFork":false,"description":"Coq code and exercises from the Coq'Art book [maintainers=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/ybertot/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/ybertot\">@ybertot</a>,<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/Casteran/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/Casteran\">@Casteran</a>]","allTopics":["exercises","coq-art","docker-coq-action","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":1,"starsCount":104,"forksCount":20,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-03T06:32:42.373Z"}},{"type":"Public","name":"jmlcoq","owner":"coq-community","isFork":false,"description":"Coq definition of JML and a verified runtime assertion checker [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["java","jml","runtime-checking","docker-coq-action","nix-action","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T10:21:05.509Z"}},{"type":"Public","name":"HighSchoolGeometry","owner":"coq-community","isFork":false,"description":"Geometry in Coq for French high school [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/thery/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/thery\">@thery</a>]","allTopics":["geometry","coq","high-school"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":16,"forksCount":2,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T10:01:56.867Z"}},{"type":"Public","name":"qarith-stern-brocot","owner":"coq-community","isFork":false,"description":"Binary rational numbers in Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/herbelin/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/herbelin\">@herbelin</a>]","allTopics":["rational-numbers","coq-library","paper-artifacts","docker-coq-action","nix-action","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":12,"forksCount":4,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T09:49:24.869Z"}},{"type":"Public","name":"buchberger","owner":"coq-community","isFork":false,"description":"Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["grobner-basis","coq-extraction","buchberger-algorithm","docker-coq-action","nix-action","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":1,"starsCount":8,"forksCount":1,"license":"GNU Lesser General Public License v2.1","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T09:36:17.360Z"}},{"type":"Public","name":"chapar","owner":"coq-community","isFork":false,"description":"A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["key-value","ocaml","causal-consistency","coq-extraction","docker-coq-action","nix-action","distributed-systems","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":4,"starsCount":32,"forksCount":7,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T09:29:37.020Z"}},{"type":"Public","name":"almost-full","owner":"coq-community","isFork":false,"description":"Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["termination","ramsey","paper-artifacts","docker-coq-action","nix-action","coq"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":0,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T09:23:44.889Z"}},{"type":"Public","name":"huffman","owner":"coq-community","isFork":false,"description":"Correctness proof of the Huffman coding algorithm in Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/palmskog/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/palmskog\">@palmskog</a>]","allTopics":["ocaml","coq","huffman-coding","huffman-tree","coq-extraction","docker-coq-action","coq-nix-toolbox"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":1,"issueCount":0,"starsCount":14,"forksCount":4,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-30T00:35:06.296Z"}},{"type":"Public","name":"gaia","owner":"coq-community","isFork":false,"description":"Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/thery/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/thery\">@thery</a>]","allTopics":["coq","set-theory","ssreflect","mathcomp","docker-coq-action","bourbaki","mathcomp-ci"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":0,"issueCount":0,"starsCount":26,"forksCount":4,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-08T15:40:59.453Z"}},{"type":"Public","name":"metaprogramming-rosetta-stone","owner":"coq-community","isFork":false,"description":"A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=<a class=\"user-mention\" data-hovercard-type=\"user\" data-hovercard-url=\"/users/yforster/hovercard\" data-octo-click=\"hovercard-link-click\" data-octo-dimensions=\"link_type:self\" href=\"https://github.com/yforster\">@yforster</a>]","allTopics":["metaprogramming","coq","coq-plugin"],"primaryLanguage":{"name":"Coq","color":"#d0b68c"},"pullRequestCount":4,"issueCount":7,"starsCount":16,"forksCount":5,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-07T19:27:07.137Z"}}],"repositoryCount":51,"userInfo":null,"searchable":true,"definitions":[],"typeFilters":[{"id":"all","text":"All"},{"id":"public","text":"Public"},{"id":"source","text":"Sources"},{"id":"fork","text":"Forks"},{"id":"archived","text":"Archived"},{"id":"template","text":"Templates"}],"compactMode":false},"title":"Repositories"}