Stars
A language with dependent data and codata types
a proof-of-concept programming language based on call-by-push-value
prototype implementation of a dependently-typed language with an extendable constraints and accompanying materials
A collaborative bibliography of work related to the theory and practice of computational effects
A proof assistant for higher-dimensional type theory
being the materials for a paper I have in mind to write about the bidirectional discipline
Eventually a practical 2-level TT-based compiler
Monorepo containing a machine-readable database of the RISC-V specification and artifact generation tools
A collection of resources for learning type theory and type theory adjacent fields.
Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
Minimal implementations for dependent type checking and elaboration
A fast functional language based on two level type theory
Demo for high-performance type theory elaboration
A place where Druid widgets come to mature before moving to the Druid repo.
A simple expressions language with polymorphic extensible row types.
A modern Prolog implementation written mostly in Rust.
Archive of LISP Machine, Inc.
The new nanopass framework; an embedded DSL for writing compilers in Scheme
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…
A programming language with static memory management based on λ-calculus