Most PL conferences moved online this year, and many are asking authors to pre-record talks to avoid livestreaming difficulties. Here are the steps we followed to record and edit our Kôika talk at PLDI 2020 and our extraction talk at IJCAR 2020. This posts covers preparing and recording the talk, adding the slides, and captioning the final video.

Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (UntypedAST) and one for typed terms (TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!

typecheck
     : UntypedAST -> option TypedAST
interp
     : TypedAST -> Value

You write a few programs…

Example well_typed := UAdd (UNat 1) (UNat 1).
Example ill_typed := UAdd (UNat 1) (UBool true).

… typecheck them:

Definition tc_good := typecheck well_typed.
Compute tc_good. (* Accepted: So far so good. *)
= Some
    {|
    tau := Nat;
    ast := TAdd (TNat 1) (TNat 1) |}
: option TypedAST

Definition tc_bad := typecheck ill_typed.
Compute tc_bad. (* Rejected: all good as well. *)
= None
: option TypedAST

… and attempt to run them:

Compute interp tc_good.
The term "tc_good" has type "option TypedAST"
while it is expected to have type "TypedAST".

D'oh! interp takes a TypedAST, but typecheck returns an option. What do we do?

A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:

Import EqNotations Vector.VectorNotations.
Compute (Vector.hd (rew (Nat.add_1_r 3) in ([1; 2; 3] ++ [4]))).
= match
    match
      Nat.add_1_r 3 in (_ = H)
      return (Vector.t nat H)
    with
    | eq_refl => [1; 2; 3; 4]
    end as c in (Vector.t _ H)
    return
      (match
         H as c0 return (Vector.t nat c0 -> Type)
       with
       | 0 =>
           fun _ : Vector.t nat 0 =>
           False -> forall x1 : Prop, x1 -> x1
       | S x => fun _ : Vector.t nat (S x) => nat
       end c)
  with
  | [] =>
      fun x : False =>
      match
        x return (forall x0 : Prop, x0 -> x0)
      with
      end
  | h :: _ => h
  end
: (fun (n : nat) (_ : Vector.t nat (S n)) => nat)
    3
    (rew [Vector.t nat] Nat.add_1_r 3 in
     ([1; 2; 3] ++ [4]))

This post shows how to work around this issue.