langston-barrett Goto Github PK

followers: 233.0 following: 214.0 repos: 108.0 gists: 12.0

Name: Langston Barrett

Type: User

Company: @GaloisInc

Bio: Researcher with experience in functional programming, formal methods, programming languages, and security.

Location: Brooklyn

Blog: https://langston-barrett.github.io

Researcher interested in functional programming, formal methods, programming languages, and security.

Projects

A comprehensive list is available here.

Highlighted Projects

MATE: A suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code using Code Property Graphs
cclyzer++: a precise and scalable global pointer analysis for LLVM code
Mogglo: Multi-language AST-based code search and rewriting tool that supports embedding Lua code in patterns
treereduce: A fast, parallel, syntax-aware test case reducer based on tree-sitter grammars
tree-splicer: Simple grammar-based test case generator (black-box fuzzer)

Datalog

cclyzer++: a precise and scalable global pointer analysis for LLVM code
dlsubst: Experimental bottom-up Datalog engine based on explicit substitutions
Duckalog: Datalog engine based on DuckDB
souffle-lint: A linter for Soufflé Datalog
treeedb: Generate Soufflé Datalog types, relations, and facts that represent ASTs from a variety of programming languages.
tree-sitter-souffle: A tree-sitter grammar for Soufflé Datalog

Fuzzing

radamsa-sys: Rust bindings for Radamsa
treereduce: A fast, parallel, syntax-aware test case reducer based on tree-sitter grammars
tree-crasher: Easy-to-use grammar-based black-box fuzzer
tree-splicer: Simple grammar-based test case generator

Tiny tools

Icemelter: Icemelter automates steps in debugging rustc internal compiler errors (ICEs)

Tiny libraries

fin-part-ord: Crate for representing finite partial orders
tree-sitter-edit: A crate for printing modified tree-sitter parse trees, intended for use in multi-language code refactoring, linting, or modification (codemod) tools

Other

contract.el: Racket-style higher-order contracts for Emacs Lisp
nixpkgs-blight: Instrument the builds of tens of thousands of open-source packages
write-yourself-a-scheme-in-agda: Like "Write Yourself a Scheme in 48 Hours", but in Agda

Writing

Langston Barrett's Projects

aeson-typescript

Generate TypeScript definition files from your ADTs

amsthm-to-anki

Translate math notes written with the amsthm package to Anki notecards!

anghabench

A benchmark suite containing 1 million compilable programs, mined from the largest public C repositories on GitHub.

anki-wikidata

Easily create high-quality Anki cards with data from Wikidata!

brick

A declarative terminal UI programming library written in Haskell

build-bom

Dynamically discover the commands used to create a piece of software

cargo-careful

Execute Rust code carefully, with extra checking along the way

category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work

company-coq

IDE extensions for Proof General's Coq mode

contract.el

Racket-style higher-order contracts for Emacs Lisp

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.