Pinned Repositories
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
HolBA
Binary analysis in HOL
mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
bitoychain
chip
Change impact analysis in Coq and OCaml
coind-sem-while
Coinductive trace-based semantics for the While language in Coq
coqdocjs
coqdocjs modified for coq-community
fitch
Certified proof checker for Fitch-style propositional logic proofs
ocaml-light
palmskog's Repositories
palmskog/fitch
Certified proof checker for Fitch-style propositional logic proofs
palmskog/coind-sem-while
Coinductive trace-based semantics for the While language in Coq
palmskog/3xp1
palmskog/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
palmskog/redblack
palmskog/algorand-verification
Formal verification of the Algorand consensus protocol
palmskog/coinduction
coinduction library for Coq
palmskog/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
palmskog/coq-elpi
Coq plugin embedding elpi
palmskog/Coq-Equations
A function definition package for Coq
palmskog/coq-primitive
palmskog/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq
palmskog/coqprime
Prime numbers for Coq
palmskog/dedekind-reals
A formalization of the Dedekind reals in Coq
palmskog/fcsl-pcm
Partial Commutative Monoids
palmskog/formalization-of-Morse-Kelley-axiomatic-set-theory
palmskog/giskard-verification
Verified model of the Giskard consensus protocol in Coq
palmskog/math-comp.github.io
https://math-comp.github.io/
palmskog/Mtac2
palmskog/negative-traces
palmskog/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
palmskog/palmskog
palmskog/palmskog.github.io
palmskog/PutnamBench
An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.
palmskog/rvdpdgraph
palmskog/sawtooth-giskard
An implementation of the Giskard consensus protocol for distributed transactions and computations.
palmskog/trustfull-demonstrator
Code for the demonstrator of the Trustfull project based on the e-voting system verificatum
palmskog/vcfloat
VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
palmskog/vscoq
A Visual Studio Code extension for Coq [maintainers=@maximedenes,@fakusb]
palmskog/www
Source files of the coq.inria.fr website (static part)