Skip to content

Instantly share code, notes, and snippets.

View L-TChen's full-sized avatar

Liang-Ting Chen L-TChen

80 followers · 141 following
View GitHub Profile
@L-TChen
L-TChen / Union.hs
Last active January 22, 2019 22:48
An imperative implementation of Union-Find algorithm in Haskell
{-# LANGUAGE BangPatterns #-}
module Union where
import Data.Ix
import Data.Array
import Data.Array.ST
import Control.Monad
import Control.Monad.ST
@L-TChen
L-TChen / Base.agda
Created February 26, 2019 14:43
Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
module Term.Base (Atom : Set)(_≟A_ : Decidable {A = Atom} (_≡_)) where
open import Relation.Nullary public
open import Data.Nat renaming (_≟_ to _≟ℕ_)
open import Data.Fin renaming (_≟_ to _≟F_) hiding (_+_; compare)
open import Data.Product hiding (map)
open import Data.List
@L-TChen
L-TChen / Playground.agda
Last active March 22, 2019 20:15
Some experiments with --prop and instance arguments
{-# OPTIONS --safe --prop --overlapping-instances #-}
module Playground where
open import Data.Nat
open import Data.List
open import Data.Bool
open import Data.Empty
open import Data.Unit
@L-TChen
L-TChen / agda-input-emacs.MD
Created July 27, 2020 11:47
Go to definitions in Agda mode combined with Evil mode in Emacs

Evil mode overwrites the mouse-2 event which is used by Agda to go to the definition of clicked identifier. To restore the desired behavioru, just add the following line after enabling Evil (require 'evil)

(define-key evil-normal-state-map [mouse-2] 'agda2-goto-definition-mouse)
@L-TChen
L-TChen / FLOLAC-STLC.lagda.md
Last active August 20, 2020 15:42

Intrinsically-typed de Bruijn representation of simply typed lambda calculus

open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
@L-TChen
L-TChen / FLOLAC-STLC-sol.agda
Created August 19, 2020 08:46
open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
hiding ([_])
infix 3 _⊢_ _=β_
infixr 7 _→̇_
@L-TChen
L-TChen / T.agda
Last active April 14, 2022 06:09
Normalization by evaluation for System T with the normalization proof and the confluence proof
{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
infix 3 _-→_ _-↛_