My CS Blog

• A (simple) proof assistant using OCaml's GADTs

  Let's build a simple proof assistant using built-in ocaml GADTs

• Weird construction using the Axiom of Choice

  Two periodic functions that sum to the identity? A function that injectively encode {x,y} into f(x) - f(y)? Yes, they are all possible, and even more!