1. 11
    Playing Around With Program and Dependent Types ☶ ml leth.io
    lthms avatar authored by lthms 1 year ago | cached | 4 comments

I used the ml tag because there is no coq tag ):.

  1.  

  2. hga avatar hga edited 1 year ago | link

    [Comment removed by author]

    1. 8
      pyon avatar pyon 1 year ago | link

      Not only is Coq written in OCaml, but Coq itself is “ML on steroids”:

      • Inductive type families generalize ML’s algebraic data types.
      • (Co)recursive function definitions (Fixpoint, Cofixpoint) are explicitly annotated as in ML (val rec, let rec), and unlike Haskell.
      • Coq’s module system is also ML-like, using signatures to hide module members or make them abstract.
      1. 3
        lthms avatar lthms edited 1 year ago | link

        Yes of course, this is why I’ve finally chosen it (:

      2. 1
        nickpsecurity avatar nickpsecurity 1 year ago | link

        I tag those with programming and math since that seems most accurate.

        1. 3
          lthms avatar lthms 1 year ago | link

          It makes sense, especially if the article focus on the “extraction” face of Coq (at least, it justifies better the programming tag).