Pinned

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 import Data.Empty                            using (⊥)

   5

   open import Data.Unit                             using (⊤; 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. provability provability Public

   Agda 5