Explore projects
-
-
Armaël Guéneau / incremental-cycles
GNU Lesser General Public License v2.1 onlyUpdated -
popstar / SAT-Equiv
GNU Affero General Public License v3.0SAT-Equiv is an equivalence checker for cryptographic protocols. It proceeds by reduction to planning problem and SAT-formula, for a bounded number of sessions.
Updated -
Yann REGIS-GIANAS / inferno
MIT LicenseA library for constraint-based Hindley-Milner type inference.
Updated -
Updated
-
Updated
-
Updated
-
Armaël Guéneau / visitors
GNU Lesser General Public License v2.1 onlyAn OCaml syntax extension (technically, a ppx_deriving plugin) which generates object-oriented visitors for traversing and transforming data structures.
Updated -
CHARGUERAUD Arthur / cfml2
Creative Commons Attribution 4.0 InternationalSeparation Logic with Characteristic Formulae Entirely within Coq
Archived 1Updated -
SCHERER Gabriel / menhir
GNU Library General Public License v2 onlyAn LR(1) parser generator for OCaml.
Updated -
Updated
-
Formally verified ML implementation of Knuth's Dancing Links algorithm, using CFML.
Updated -
BAUDIN Lucas / why3
GNU Lesser General Public License v2.1 onlyWhy3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.
Updated -
implementation and metatheory of time credits and time receipts in Iris / Coq
Updated -
Benedikt Becker / why3
GNU Lesser General Public License v2.1 onlyWhy3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.
Updated -
Formalizations accompanying my thesis "Extending Type Theory with Syntactical Models".
Updated -
skeletons / Necro Library
GNU General Public License v3.0 onlyPrimary library for necro with standard tools (parse, type check, print, and transform Skeletal Semantics)
Updated -
BLANCHET Bruno / CryptoVerif
CeCILL-B Free Software License AgreementUpdated -
belenios / belenios
GNU Affero General Public License v3.0Verifiable online voting system http://www.belenios.org
Updated -
Ocan Sankur / symrob
GNU General Public License v3.0 or laterTool for timed automata verification and robustness analysis
Updated