acorrenson
PhD candidate at CISPA. Working on formally verified formal methods.
ENS Rennes, Saarland University, CISPASaarbrücken
Pinned Repositories
automatik
A library of formalized automaton algorithms
cqfd
A why3 certified prover for propositional logic
Maybe
A tiny probabilist functional language
metamatix
A verified implementation of a metamath proof checker
minilog
A verified Implementation of a mini prolog
modulus
A constraint solver built from scratch in OCaml
Oratio
Translate natural deduction proofs into natural language.
owl
A mini language for logic programming
SATurne
Tiny verified SAT-solver
WiSE
A formally verified bug finder
acorrenson's Repositories
acorrenson/minilog
A verified Implementation of a mini prolog
acorrenson/WiSE
A formally verified bug finder
acorrenson/automatik
A library of formalized automaton algorithms
acorrenson/metamatix
A verified implementation of a metamath proof checker
acorrenson/Maybe
A tiny probabilist functional language
acorrenson/ocallm
Training a (tiny) language model in OCaml, from scratch
acorrenson/bayes
Trying to understand basic ML stuff
acorrenson/Defaultt
An attempt at formalizing default logic in Coq
acorrenson/minilia
Minimalistic OCaml API to send LIA queries to Z3
acorrenson/3valued
3 valued logic in Coq
acorrenson/acorrenson.github.io
Personnal Website
acorrenson/catala
Programming language for literate programming law specification
acorrenson/cfloat
Messing arround with floats in C
acorrenson/color
Coq library on rewriting theory and termination
acorrenson/coqffi
Coq to OCaml FFI made easy [maintainer=@lthms]
acorrenson/coqinit
A script to initialise a new Coq project.
acorrenson/easyprint
Double sided printing for standard printers
acorrenson/gitignore
A collection of useful .gitignore templates
acorrenson/InteractionTrees
A Library for Representing Recursive and Impure Programs in Coq
acorrenson/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
acorrenson/master_thesis_data
acorrenson/mathlib
Lean mathematical components library
acorrenson/minibug
Concise and documented COq formalization of a symbolic bug finder for IMP
acorrenson/multiset
A self-contained Coq library of multisite
acorrenson/pravda
Pravda is a tool for teaching formal logic.
acorrenson/simplebnf
Simple Backus–Naur form (BNF) LaTeX package
acorrenson/smtcoq
Communication between Coq and SAT/SMT solvers
acorrenson/smtcoq-api
An API to interact with SMTCoq
acorrenson/typst
A new markup-based typesetting system that is powerful and easy to learn.
acorrenson/verified-static-analyzer
A small & simple WIP verified static analyzer