Skip to content

@TypicalMath TypicalMath

Change the repository type filter

All

    Repositories list

    8 repositories

    • lambda2

      Public
      An implementatino of λ2 system, with some simple properties
      Rocq Prover
      •1•0•0•0•Updated Sep 5, 2025Sep 5, 2025

    • stl

      Public
      The Logic of Spacetime in Coq
      coqlogicsequent-calculus
      coqlogicsequent-calculus
      Coq
      •0•0•0•0•Updated Jun 16, 2023Jun 16, 2023

    • cpc

      Public
      A try to implement the completeness theorem of classical propositional logic
      Coq
      •2•0•0•1•Updated Apr 10, 2023Apr 10, 2023

    • hilbert-gentzen

      Public
      Every Hilbert-style proof has a Natural couterpart, and vice versa.
      Coq
      •1•0•0•0•Updated Jul 25, 2022Jul 25, 2022

    • subst-interpol

      Public
      Uniform Interpolation for some Substructural Logics (work in progress)
      coqcoq-formalization
      coqcoq-formalization
      Coq
      •0•2•0•0•Updated Apr 12, 2020Apr 12, 2020

    • nat-finset

      Public
      Re-inventing finite sets (because (learning) ssreflect is overkill)
      Coq
      •0•0•0•0•Updated Dec 25, 2019Dec 25, 2019

    • prop-calc

      Public
      Propositional Calculus in Coq by Floris van Doorn
      coqlogic
      coqlogic
      Coq
      •0•3•0•0•Updated Jun 14, 2019Jun 14, 2019

    • ruitenburg1984

      Public
      A https://git8.cs.fau.de/software/ruitenburg1984/ fork
      Coq
      •0•0•0•0•Updated May 20, 2019May 20, 2019