tjhao

tjhao's Stars

• lexi-lambda/eff

  🚧 a work in progress effect system for Haskell 🚧

  Language:Haskell1242

• meithecatte/busycoq

  Busy Beaver deciders backed by Coq proof

  Language:Coq396

• sweirich/pi-forall

  A demo implementation of a simple dependently-typed language

  Language:Haskell56489

• jsiek/deduce

  A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.

  Language:Python593

• juniorxxue/contextual-typing

  Contextual Typing, formalised in Agda

  Language:Agda9

• Lysxia/system-F

  Formalization of the polymorphic lambda calculus and its parametricity theorem

  Language:Coq332

• mre/idiomatic-rust

  🦀 A peer-reviewed collection of articles/talks/repos which teach concise, idiomatic Rust.

  Language:Rust6.6k205

• rust-lang/rust-by-example

  Learn Rust with examples (Live code editor included)

  Language:Handlebars7.1k1.4k

• formal-land/coq-of-rust

  Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

  Language:Coq42817

• AnthonyCalandra/modern-cpp-features

  A cheatsheet of modern C++ language and library features.

  19.8k2.1k

• rust-unofficial/too-many-lists

  Learn Rust by writing Entirely Too Many linked lists

  Language:Rust3.2k281

• mainmatter/100-exercises-to-learn-rust

  A self-paced course to learn Rust, one exercise at a time.

  Language:Rust6.3k1.1k

• rust-lang/rustlings

  :crab: Small exercises to get you used to reading and writing Rust code!

  Language:Rust54.6k10.2k

• Zdancewic/linearity

  Formalization of Linear Logic and Related Programming Languages Metatheory

  Language:Coq102

• coq-community/autosubst

  Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

  Language:Coq5214

• DEIS-Tools/PDAAAL

  PushDown Automata - AALborg

  Language:C++51

• compiler-explorer/compiler-explorer

  Run compilers interactively from your web browser and interact with the assembly

  Language:TypeScript16.5k1.8k

• klee/klee

  KLEE Symbolic Execution Engine

  Language:C++2.7k683

• mpark/patterns

  This is an experimental library that has evolved to P2688

  Language:C++66631

• electronicarts/EASTL

  EASTL stands for Electronic Arts Standard Template Library. It is an extensive and robust implementation that has an emphasis on high performance.

  Language:C++8.3k945

• coq-community/dblib

  Coq library for working with de Bruijn indices [maintainer=@KevOrr]

  Language:Coq304

• google/pytype

  A static type analyzer for Python code

  Language:Python4.8k281

• Z3Prover/z3

  The Z3 Theorem Prover

  Language:C++10.4k1.5k

• sampsyo/ppl-intro

  probabilistic programming for PL folks

  Language:Makefile15220

• IUCompilerCourse/Essentials-of-Compilation

  A book about compiling Racket and Python to x86-64 assembly

  Language:TeX1.3k143

• ocaml-multicore/ocaml-effects-tutorial

  Concurrent Programming with Effect Handlers

  Language:OCaml66737

• XSnow/TamingMerge

  Coq formalization for Taming the Merge Operator

  Language:Coq41

• XSnow/ECOOP2020

  A Type-Directed Operational Semantics for a Calculus with a Merge Operator

  Language:Coq72

• rocq-archive/paradoxes

  Paradoxes in Set Theory and Type Theory

  Language:Coq11

• tssovi/grokking-the-object-oriented-design-interview

  Language:Python5k2.4k