Pinned Repositories
cantor
constructive formalization of cantor's theorem about dense linear orders without endpoints
combinator-confluence
A proof of confluence for combinatory logic
coq-project
My project using Coq to prove Post's Theorem.
coqchess
coqchesstable
coqtbgen
formally verified endgame tablebase generator in coq
emarzion.github.io
my blog
IFOL
Coq formalization of intuitionistic first-order logic
Linear-Logic-Proof-Assistant
Sequent calculus based proof assistant for ILL
SystemT
An interpreter for Gödel's System T
emarzion's Repositories
emarzion/SystemT
An interpreter for Gödel's System T
emarzion/Linear-Logic-Proof-Assistant
Sequent calculus based proof assistant for ILL
emarzion/coqtbgen
formally verified endgame tablebase generator in coq
emarzion/cantor
constructive formalization of cantor's theorem about dense linear orders without endpoints
emarzion/IFOL
Coq formalization of intuitionistic first-order logic
emarzion/combinator-confluence
A proof of confluence for combinatory logic
emarzion/coq-project
My project using Coq to prove Post's Theorem.
emarzion/coqchess
emarzion/coqchesstable
emarzion/emarzion.github.io
my blog
emarzion/hm
Definitional interpreter for Hindley-Milner in Coq
emarzion/lc-self-interpreter
Formally verified self-interpreter for untyped lambda calculus
emarzion/games
Games library
emarzion/misc
emarzion/PathORAM
Formalizing the PathORAM implementation by Chris et al.