hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

craigfe

#!/usr/bin/env sh

# A .merlin must be present nearby the file.
# With dune it can be generated by calling `dune build @check`.

FILE="$1"

dune build @check
ocamlmerlin single dump -what ppxed-source -filename "$FILE" < "$FILE" | jq -r '.value' | ocamlformat --name="$FILE" -

Aerijo

\documentclass[a4paper]{article}
\input{./hoare.tex}

\begin{document}
\begin{hoare}
    \heq[a]{m * (a-b) > 0}{n := a-b}{m * n > 0}{\A}
    \heq[b]{1 * (a-b) > 0}{m := 1}{m * (a-b) > 0}{\A}
    \heq[c]{a > b}{m := 1}{m * (a-b) > 0}{\PrE(b)}
    \heq[d]{a > b}{m := 1; n := a-b}{m * n > 0}{\Seq(c, a)}
\end{hoare}

45deg

type prop =
 True |
 Var of char |
 And of prop * prop |
 Not of prop |
 N of prop |
 U of prop * prop

(* slow! *)
let eventually p = U (True, p)

killercup

/*
 * I add this to html files generated with pandoc.
 */

html {
  font-size: 100%;
  overflow-y: scroll;
  -webkit-text-size-adjust: 100%;
  -ms-text-size-adjust: 100%;
}

sebfisch

Delimited Continuations

Delimited continuations manipulate the control flow of programs. Similar to control structures like conditionals or loops they allow to deviate from a sequential flow of control.

We use exception handling as another example for control flow manipulation and later show how to implement it using delimited continuations. Finally, we show that nondeterminism can also be expressed using delimited continuations.

Exception Handling