A proof that Coq typeclass resolution is Turing-complete
-
Updated
Apr 16, 2023 - 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. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
A proof that Coq typeclass resolution is Turing-complete
A Coq library for abstract syntactical reasoning
OCaml module of Nijn to generate coq scripts for checking termination proofs of higher-order rewriting systems.
A verification tool developed in Coq for analyzing cloud block storage
Calvin Talks Types
Configuring Proof General for use with Coq is hard and the defaults suck. This is a simple baseline configuration for Emacs.
Run `coqc` and print out colorized Coq error location information
A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.
My solution of《software fundations I》,some proof may be trivial...
Specification, formalization and verification of the XC function from ex lambda calculus in Coq.
Źródła mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych takich.
Extension of atomic triples in Iris with atomic postconditions and formal verification of the Lazy JellyFish skip list
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 3 months ago