#
Starred repositories
Dafny is a verification-aware programming language
Research prototype tool for modular formal verification of C and Java programs
CS316 "Functional Programming" lecture notes
Kotlin implementation of CFL Reachability algorithm for pointer analysis in C++ and Java programs
2
Updated Apr 9, 2023
Preprocessor for typesetting Haskell sources with LaTeX
A verified implementation of a metamath proof checker
Tricks you wish the Coq manual told you [maintainer=@tchajed]
OCaml library for manipulating OpenQASM Abstract Syntax Tree
A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.
A demo implementation of a simple dependently-typed language
Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.
Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of fu…
Language Server Protocol implementation for Swift and C-based languages
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Lenses, Folds, and Traversals - Join us on web.libera.chat #haskell-lens
An efficient compact, immutable byte string type (both strict and lazy) suitable for binary or 8-bit character data.
A multilingual package manager for Arch Linux and the AUR.
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 develo…
