Pinned Loading

1. ogs ogs Public

   operational game semantics, formalized in Coq

   Coq 2

2. mu-mu-tilde mu-mu-tilde Public

   A mini formalization of μμ͂ and classical realizability

   Coq 3

3. induction-recursion induction-recursion Public

   formalization of ornaments on indexed inductive-recursive definitions

   8

4. lambda-encoding lambda-encoding Public

   Deriving induction principles for lambda-encoded datatypes in Coq

   Coq 1

5. grothendieck-cern grothendieck-cern Public

   Alexander Grothendieck's 1972 talk at CERN, on scientific research

   54 5

6. A very cute demo of smart constructo... A very cute demo of smart constructors for pure λ-calculus (some sort of HOAS to intrinsically scoped De-Bruijn transform) by Conor McBride which i ported to Coq.

   1

   -- Source: Conor McBride

   2

   -- https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda

   3

   module Jigger where

   4

   5

   data Nat : Set where