A course on Rakudo and NQP internals, developed by Edument AB.

Contextual types meet mechanized metatheory!

Replacement board for Casio Calculator Watches using the CC430F6147

Mirror of https://gitlab.redox-os.org/redox-os/redox

A collaborative bibliography of work related to the theory and practice of computational effects

An experimental type checker for a modal dependent type theory.

A statically-typed linear functional language with graded modal types for fine-grained program reasoning

Compiler for the Mirth programming language.

An interactive theorem prover based on lambda-tree syntax

A modern proof language

Presentation software based on nested, zoomable canvases and live code.

Lean library for Universal Algebra

An experimental category theory library for Lean

Functional programming with fewer indirections

A friendly effect system for Haskell

OCaml & Reason support for Visual Studio Code

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

Movitz: a Common Lisp x86 development platform

Collection of ATS goodness

A tiny 32 bit kernel written in ATS

some kind of operating system

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

A small implementation of a proof refinement logic.

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

A statically-typed, functional typesetting system

secret project

The best way to write secure and reliable applications. Write nothing; deploy nowhere.

Observational Type Theory as an Agda library