bjartem

bjartem's Stars

• coq/coq

  Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

  Language:OCaml4.9k10410.1k661

• ghcjs/ghcjs

  Haskell to JavaScript compiler, based on GHC

  Language:Haskell2.6k75680186

• cksystemsteaching/selfie

  An educational software system of a tiny self-compiling C compiler, a tiny self-executing RISC-V emulator, and a tiny self-hosting RISC-V hypervisor.

  Language:Jupyter Notebook2.4k6192312

• leanprover/lean3

  Lean Theorem Prover

  Language:C++2.2k1161.1k217

• corkami/pocs

  Proof of Concepts (PE, PDF...)

  Language:Assembly1.5k757198

• CakeML/cakeml

  CakeML: A Verified Implementation of ML

  Language:Standard ML9854450186

• secure-software-engineering/phasar

  A LLVM-based static analysis framework.

  Language:C++95130187142

• rems-project/sail

  Sail architecture definition language

  Language:Isabelle64936343119

• clarkerubber/irwin

  irwin - the protector of lichess from all chess players villainous

  Language:Python513251043

• ProofGeneral/PG

  This repo is the new home of Proof General

  Language:Emacs Lisp4951353790

• polyml/polyml

  Poly/ML

  Language:Standard ML4904212447

• tchajed/coq-tricks

  Tricks you wish the Coq manual told you

  Language:Coq484261420

• peikexin9/deepxplore

  DeepXplore code release

  Language:Python3953626146

• ott-lang/ott

  The Ott tool for writing definitions of programming languages and calculi

  Language:OCaml351155546

• coq-community/awesome-coq

  A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

  332141220

• mietek/sf

  Mirror of Software Foundations in PDF

  Language:HTML29711556

• antalsz/hs-to-coq

  Convert Haskell source code to Coq source code

  Language:Coq2791614727

• cpitclaudel/alectryon

  A collection of tools for writing technical documents that mix Coq code and prose.

  Language:HTML243117734

• tech-srl/Nero

  Code and resources for the paper: "Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs"

  Language:Python188111722

• PatrickMassot/leanblueprint

  plasTeX plugin to build formalization blueprints.

  Language:Python175102230

• jwiegley/coq-haskell

  A library for formalizing Haskell types and functions in Coq

  Language:Coq16812410

• kmill/lean4-raytracer

  A simple raytracer written in Lean 4

  Language:Lean132735

• rems-project/lem

  Lem semantic definition language

  Language:OCaml132202215

• calccrypto/tar

  A simple tar implementation in C

  Language:C11751135

• cpitclaudel/academic-poster-template

  An HTML+CSS template for making more accessible posters

  Language:Less823530

• plclub/hs-to-coq

  Convert Haskell source code to Coq source code.

  Language:Coq79131899

• maximedenes/coq-amd64

  Language:Coq22604

• hephaestus-pl/coqfj

  A mechanized proof of type safety for Featherweight Java using Coq

  Language:Coq16511

• GaloisInc/simple-tar

  A very simple tar archive processing library

  Language:Haskell1131

• guibou/MineSweeper

  Haskell Reflex mine sweeper

  Language:Haskell2