Pinned

1. formal-topology-in-UF

   Formal Topology in Univalent Foundations (WIP).

   Agda 20 2

2. simplc

   A tiny compiler for a security-typed imperative language with a formalised proof of noninterference-preservation.

   Agda 12

3. abt

   Ocaml port of CMU's ABT library (with various modifications).

   OCaml 9 1

4. grammar-inference

   Learning rigid grammars in Haskell.

   Haskell 24 2

5. sequents

   Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

   Standard ML 12

6. sml-system-t

   SML implementation of System T from PFPL.

   Standard ML 10 1