Popular repositories Loading

1. ipc2 ipc2 Public archive

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

   Coq 3

2. lambda-cap lambda-cap Public archive

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

   Coq

3. cls-fsharp cls-fsharp Public archive

   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. hom-it-inh hom-it-inh Public

   Undecidability of higher-order matching based on intersection type inhabitation.

   TeX