Skip to content
View acorrenson's full-sized avatar
🐓
Proving Large Programs in Coq
🐓
Proving Large Programs in Coq
146 followers · 257 following

Achievements

Achievement: StarstruckAchievement: Pull Sharkx3Achievement: Arctic Code Vault Contributor

Achievements

Achievement: StarstruckAchievement: Pull Sharkx3Achievement: Arctic Code Vault Contributor

Organizations

@codeanonorg
Block or Report

Block or report acorrenson

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

  • acorrenson.github.io Public

    Personnal Website

    HTML Updated Jul 26, 2024

  • myopencl Public

    A tiny wrapper arround OpenCL C API

    C 1 MIT License Updated Jun 11, 2024

  • ocallm Public

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

    OCaml 4 MIT License Updated Jun 2, 2024

  • minilia Public

    Minimalistic OCaml API to send LIA queries to Z3

    OCaml 1 MIT License Updated May 2, 2024

  • InteractionTrees Public

    Forked from DeepSpec/InteractionTrees

    A Library for Representing Recursive and Impure Programs in Coq

    Coq MIT License Updated Apr 19, 2024

  • pravda Public

    Forked from livrelogique/pravda

    Pravda is a tool for teaching formal logic.

    TypeScript GNU General Public License v2.0 Updated Mar 14, 2024

  • Maybe Public

    A tiny probabilist functional language

    OCaml 6 MIT License Updated Mar 12, 2024

  • master_thesis_data Public

    Coq MIT License Updated Jan 12, 2024

  • 3valued Public

    3 valued logic in Coq

    Coq MIT License Updated Jan 9, 2024

  • minibug Public

    Concise and documented COq formalization of a symbolic bug finder for IMP

    Coq MIT License Updated Jan 4, 2024

  • multiset Public

    A self-contained Coq library of multisite

    Coq MIT License Updated Aug 29, 2023

  • WiSE Public

    A formally verified bug finder

    Python 13 1 MIT License Updated Aug 21, 2023

  • bayes Public

    Trying to understand basic ML stuff

    Python 1 MIT License Updated Jul 7, 2023

  • typst Public

    Forked from typst/typst

    A new markup-based typesetting system that is powerful and easy to learn.

    Rust Apache License 2.0 Updated May 1, 2023

  • metamatix Public

    A verified implementation of a metamath proof checker

    Coq 9 1 Creative Commons Zero v1.0 Universal Updated Apr 16, 2023

  • color Public

    Forked from fblanqui/color

    Coq library on rewriting theory and termination

    Coq Other Updated Mar 15, 2023

  • verified-static-analyzer Public

    Forked from Chaarlesss/verified-static-analyzer

    A small & simple WIP verified static analyzer

    Coq Updated Mar 13, 2023

  • catala Public

    Forked from CatalaLang/catala

    Programming language for literate programming law specification

    OCaml Apache License 2.0 Updated Jan 15, 2023

  • mathlib Public

    Forked from leanprover-community/mathlib3

    Lean mathematical components library

    Lean Apache License 2.0 Updated Dec 7, 2022

  • minilog Public

    A verified Implementation of a mini prolog

    Coq 13 1 MIT License Updated Nov 27, 2022

  • smtcoq-api Public

    Forked from smtcoq/smtcoq-api

    An API to interact with SMTCoq

    OCaml Other Updated Nov 17, 2022

  • smtcoq Public

    Forked from smtcoq/smtcoq

    Communication between Coq and SAT/SMT solvers

    OCaml Other Updated Nov 17, 2022

  • simplebnf Public

    Forked from Zeta611/simplebnf

    Simple Backus–Naur form (BNF) LaTeX package

    TeX MIT License Updated Nov 15, 2022

  • coqinit Public

    A script to initialise a new Coq project.

    OCaml MIT License Updated Nov 12, 2022

  • coqffi Public

    Forked from coq-community/coqffi

    Coq to OCaml FFI made easy [maintainer=@lthms]

    OCaml MIT License Updated Nov 3, 2022

  • cfloat Public

    Messing arround with floats in C

    MIT License Updated Oct 18, 2022

  • Defaultt Public

    An attempt at formalizing default logic in Coq

    Coq 1 MIT License Updated Oct 4, 2022

  • gitignore Public

    Forked from github/gitignore

    A collection of useful .gitignore templates

    Creative Commons Zero v1.0 Universal Updated Oct 4, 2022

  • easyprint Public

    Double sided printing for standard printers

    OCaml MIT License Updated Oct 3, 2022

  • automatik Public

    A library of formalized automaton algorithms

    automata algorithms graph coq coq-formalization formal-verification formal-proofs
    Coq 9 1 MIT License Updated Aug 3, 2022