임기정

portfolio. My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.

DschingisKhan. He Reiter, Ho Reiter, He Reiter, Immer weiter!

ppap. Project Putting All Power!

PlanHol. a Programming LANguage with Higher-Order Logic

LogicStudy. my notes for mathematical logic

V9. capstone

Homeworks. Haskell

Fol-archived. A New Coq Formalisation of Classical First-Order Logic with Proofs of the Soundness and Completeness Theorems

KWON. Haskell

proof. Coq

LoL. Coq

Ordinal. Rocq Prover

cxxs. C++ srcs

Capstone. C++