The Scala 3 compiler, also known as Dotty.

Terra is a low-level system programming language that is embedded in and meta-programmed by the Lua programming language.

formalization of the Dependent Object Types (DOT) calculus

An optional type system for Clojure

Concurrent Programming with Effect Handlers

Scheme Scripting Engine

Demo for high-performance type theory elaboration

being the materials for Summer 2013's course

A small compiler for PCF

Normalization by Evaluation for Martin-Löf Type Theory

implementation of Pure Type Systems (PTS) in Rust.

Normalization by evaluation for Martin-Löf Type Theory with dependent records

🌙 LunarVim is an IDE layer for Neovim. Completely free and community driven.

A file explorer tree for neovim written in lua

A use-package inspired plugin manager for Neovim. Uses native packages, supports Luarocks dependencies, written in Lua, allows for expressive config

A library for formalizing Haskell types and functions in Coq

Agda formalisation of the Introduction to Homotopy Type Theory

Frank compiler

Drafts, notes and resources for adding linear typing to GHC.

A formalization of continuation-passing style calculi in Coq [WIP]

Multicore OCaml

Formalizations of Gradually Typed Languages in Agda

A pure type system implemented in OCaml

A Verified Compiler for Gallina, Written in Gallina

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

Examples of how to create colorful, annotated equations in Latex using Tikz.

OCaml の日本語での情報

An implementation of Linear Lambda Calculus.

Brainfuck formalized in Coq