Pinned Loading

1. ltac2-tutorial ltac2-tutorial Public

   A simple Ltac2 tutorial that covers the very basics.

   Coq 5

2. mltt-consistency mltt-consistency Public

   Logical relation for predicative CC omega with booleans and an intensional identity type

   TeX 5 2

3. TPOSR TPOSR Public

   Autosubst 2 reimplementation of the paper "Pure Type System conversion is always typable"

   Coq 1

4. system-f-omega system-f-omega Public

   Strong normalization and parametricity for System Fω in Coq

   Coq 1 1

5. system-t-per system-t-per Public

   Coq

6. takahashi-factorization takahashi-factorization Public

   A proof of factorization using Takahashi's method

   Coq 1 1