Pinned Repositories
Proof-Theory-of-Riesz-Spaces-and-Modal-Riesz-Spaces
Implementation of the hypersequent calculii HR and HMR introduced in the article "Proof Theory of Riesz Spaces and Modal Riesz Spaces" (https://arxiv.org/abs/2004.11185).
riesz-logic
clucas26e4.github.io
formalisedGA
Formalized proofs of soundness and completeness of a hypersequent calculus for lattice-ordered Abelian groups
JotunnModStub
Valheim mod skeleton using Jötunn
List_Permutation
M-elimination
Implementation of the proof of the M-elimination theorem for the system MGA in Agda
ollibs
Add-ons for the Coq Standard Library
progress_knight_2
Mod
ramics_archimedean
Coq formalization for the article "Free Modal Riesz Spaces are Archimedean: a Syntactic Proof"
clucas26e4's Repositories
clucas26e4/List_Permutation
clucas26e4/progress_knight_2
Mod
clucas26e4/clucas26e4.github.io
clucas26e4/JotunnModStub
Valheim mod skeleton using Jötunn
clucas26e4/ramics_archimedean
Coq formalization for the article "Free Modal Riesz Spaces are Archimedean: a Syntactic Proof"
clucas26e4/riesz-logic
clucas26e4/Proof-Theory-of-Riesz-Spaces-and-Modal-Riesz-Spaces
Implementation of the hypersequent calculii HR and HMR introduced in the article "Proof Theory of Riesz Spaces and Modal Riesz Spaces" (https://arxiv.org/abs/2004.11185).
clucas26e4/ollibs
Add-ons for the Coq Standard Library
clucas26e4/yalla
Yet Another deep embedding of Linear Logic in Coq
clucas26e4/M-elimination
Implementation of the proof of the M-elimination theorem for the system MGA in Agda
clucas26e4/formalisedGA
Formalized proofs of soundness and completeness of a hypersequent calculus for lattice-ordered Abelian groups