임기정 KiJeong-Lim

I'm a master's/Ph.D. student majoring in Computer Science and Engineering at Yonsei University.

KiJeong-Lim / hello.v

Last active September 3, 2020 07:14

	Require Export Omega.
	Require Export List.

	Axiom classic : forall P : Prop, P \/ not P.

	Module ListTheory.

	Section General.

	Import ListNotations.

KiJeong-Lim / hopu.hs

Created July 20, 2020 15:51

Higher-Order Pattern Unification

	import Control.Monad.IO.Class
	import Control.Monad.Trans.Class
	import Control.Monad.Trans.Except
	import Control.Monad.Trans.State.Strict
	import Data.IORef
	import qualified Data.List as List
	import qualified Data.Map.Strict as Map
	import qualified Data.Set as Set
	import Data.Unique

KiJeong-Lim / ndc.mod

Created July 13, 2020 13:43

natural deduction checker

	module ndc.

	kind parity type -> type -> type.
	type pair (A -> B -> parity A B).

	kind term type.
	type fapp (string -> list term -> term).

	kind formula type.
	type atom (string -> list term -> formula).