Pinned Loading

1. Formal Topology in Univalent Foundations (WIP).

   CSS 37 2

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

   Agda 16

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

   OCaml 9 2

4. Learning rigid grammars in Haskell.

   Haskell 24 2

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

   Standard ML 27

6. SML implementation of System T from PFPL.

   Standard ML 11 1