Popular repositories Loading

1. ipc2 ipc2 Public

   Reduction from Diophantine equations to provability in IPC2 / System F.

   Coq 3

2. lambda-cap lambda-cap Public

   Reduction from simple semi-Thue system rewriting to inhabitation in the Coppo-Dezani type assignment system.

   Coq

3. cls-fsharp cls-fsharp Public

   Implementation of the Combinatory Logic Synthesizer algorithm in F#

   F#

4. coq-library-undecidability coq-library-undecidability Public

   Forked from uds-psl/coq-library-undecidability

   A library of formalised undecidable problems in Coq

   Coq

5. coq coq Public

   Forked from rocq-prover/rocq

   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 develo…

   OCaml

6. GeoCoq GeoCoq Public

   Forked from GeoCoq/GeoCoq

   A formalization of geometry in Coq based on Tarski's axiom system

   Coq