You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
Lim, Kijeong. "A New Coq Formalisation of Classical First-Order Logic with Proofs of the Soundness and Completeness Theorems." 한국정보과학회 학술발표논문집 (2024): 1175-1177.
DschingisKhan
Coq Codes
Pdf
Pdf files
ppap
Haskell Codes
About
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.