Pinned Loading

1. Normalization by evaluation for Syst...Normalization by evaluation for System T with the normalization proof and the confluence proof

   1

   {- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.

   2

    Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

   3

   4

   open importData.Emptyusing (⊥)

   5

   open importData.Unitusing (⊤; tt)

2. An implementation of McBride's struc...An implementation of McBride's structural first-order unification algorithm in Haskell. Tested on GHC 8.4.4

   1

   {-# LANGUAGE FlexibleContexts, FlexibleInstances #-}

   2

   {-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 

   3

   {-# LANGUAGE GADTs, StandaloneDeriving #-}

   4

   {-# LANGUAGE Safe #-}

   5

3. provabilityprovabilityPublic

   Agda 6