Pinned Repositories
fav-ssr
Functional Algorithms Verified in SSReflect
idris-linear
Experiments with linear types
modal-types
Experiments with modal types
opticui-elm-architecture
Elm arch guide in OpticUI
sequent-calc
Experiments with sequent calculi
sequent-calc-talk
Code for the "Logic, machines and sequent calculus" talk
idris-tparsec
TParsec - Total Parser Combinators in Idris
software-foundations
Software Foundations in Idris
idris-bi
Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
code
Proof theory seminar
clayrat's Repositories
clayrat/fav-ssr
Functional Algorithms Verified in SSReflect
clayrat/logrel-guarded
Guarded logical relations
clayrat/guarded-cm
Experiments with guarded recursion
clayrat/ipc-ssr
Weich's Intuitionistic Solver in SSReflect
clayrat/refutation
Refutation and paraconsistent calculi
clayrat/resolution-ssr
Resolution in SSReflect
clayrat/dialectica
Dialectica translations
clayrat/guarded-termination
Termination proofs for guarded algorithms
clayrat/provability-cm
Port of S4+GL semantics to cubical-mini
clayrat/clayrat.github.io
clayrat/Coherence-of-Heyting-arithmetic
Coherence of Heyting's first order arithmetic in Coq: "Proof assistants" project at LMFI, Paris-Diderot University (teacher: Pierre Letouzey)
clayrat/coq-refinements
clayrat/cubical-mini
clayrat/guarded-automata
Automata in guarded type theory
clayrat/guarded-lh
Guarded LiquidHaskell
clayrat/guarded-objects
Objects via guarded types
clayrat/guarded-search
Search algorithms in guarded/clocked type theory
clayrat/haskell-chart
A 2D charting library for haskell
clayrat/Idris2
A purely functional programming language with first class types
clayrat/ipc
Intuitionistic Propositional Checker
clayrat/liquid-fixpoint
Horn Clause Constraint Solving for Liquid Types
clayrat/liquidhaskell
Liquid Types For Haskell
clayrat/math-comp
Mathematical Components
clayrat/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
clayrat/practical-fm
A gently curated list of companies using verification formal methods in industry
clayrat/refhoare-idr
Hoare-Logic Style Refinement Types
clayrat/reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
clayrat/smtcoq
Communication between Coq and SAT/SMT solvers
clayrat/SymmetryBook
This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
clayrat/TreeAutomataFormalization