Arthur Correnson

SATurne. Tiny verified SAT-solver

owl. A mini language for logic programming

minilog. A verified Implementation of a mini prolog

WiSE. A formally verified bug finder

modulus. A constraint solver built from scratch in OCaml

cqfd. A why3 certified prover for propositional logic

metamatix. A verified implementation of a metamath proof checker

automatik. A library of formalized automaton algorithms

Oratio. Translate natural deduction proofs into natural language.

Maybe. A tiny probabilist functional language

lili. Minimalist proof checker based on a simply typed lambda-calculus

Algos. Some usefull algorithms implemented as a robust collection of modules for OCaml, C, Python and more

BF. A Coq Formalization of the Brainfuck programming language

ocallm. Training a (tiny) language model in OCaml, from scratch

hyco-popl-2025. Coq developpement accompanying the paper "Coinductive Proofs for Temporal Hyperliveness" to appear at POPL 2025

strange_algebra. Resolve boolean system of equations using Gauss algorithm.

ocaml_web_ui. An example of web application written in OCAML

superChip8. an emulator for the chip-8 system written in C

Pym-s. Python with a sweet functionnal taste

flow. An abstract interpreter

kind2coq. A experimental compiler from Kind (Core) to Coq

article-bf.

neutron. A Coq-certified preprocessor for boolean logic formulae

mfc. My First Compiler

deep_checker. Final project for the statistics class at ENS

Djinn. OCaml binding for the Tinn library

superChip8-compiler. An experimental compiler for chip-8 asm.

Puzzle. An OCaml DSL for problem solving based on symbolic AI techniques

code.sflk. Vscode extension for sflk

systemf. A minimalistic implementation of system F in rust

myopencl. A tiny wrapper arround OpenCL C API

BinarySearchTree-ocaml. BinarySearchTree (BST) implementation in ocaml

xxbf. Brainfuck compiler and interpreter

Defaultt. An attempt at formalizing default logic in Coq

PetitGuideDesNombresFlottants. Un mini-livre open-source pour mieux comprendre les nombres flottants

bayes. Trying to understand basic ML stuff

minilia. Minimalistic OCaml API to send LIA queries to Z3

passerine. A small extensible programming language designed for concise expression with little code.

Ministrel. A toy implementation of a synchronous programming language inspired by Esterel

ISN-PROJETFINAL. Processing

ArcoexBot. A simple Discord bot aimed at arbitrary code execution.

tableaunoir.github.io. An online blackboard with fridge magnets