Pinned Repositories
gator
Geometry types
best-of-popl
Best of POPL (BOP) Reading Group Memoirs
flambda-backend
The Flambda backend project for OCaml
icfp22-layered-monadic-interpreters
artifact for ICFP'22 paper "Formal Reasoning About Layered Monadic Interpreters"
logrel-iris
mini-pi
velliris
gnocchi
Basic Minecraft-like procedurally generated world using WebGL and WebSockets
vellvm
The Vellvm (Verified LLVM) coq development.
helix
Formally verified operator language and rewriting engine for high-performance computing
euisuny's Repositories
euisuny/best-of-popl
Best of POPL (BOP) Reading Group Memoirs
euisuny/icfp22-layered-monadic-interpreters
artifact for ICFP'22 paper "Formal Reasoning About Layered Monadic Interpreters"
euisuny/chan-iris
iris chan
euisuny/logrel-iris
euisuny/mini-pi
euisuny/velliris
euisuny/flambda-backend
The Flambda backend project for OCaml
euisuny/acm-paper-template
Skeleton template for ACM papers (with additional flair for Coq-related content)
euisuny/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
euisuny/dotfiles
lots of dots and files
euisuny/dprop
A deep embedding of propositional logic in Coq
euisuny/euisuny.github.io
personal website
euisuny/Glowstone
A fast, customizable and compatible open source Minecraft server.
euisuny/HoTT
Homotopy type theory
euisuny/hs-to-coq
Convert Haskell source code to Coq source code
euisuny/iris_cola
Short proof that bi logic used in Iris forms a complete lattice in two ways
euisuny/llvm-pass-skeleton
example LLVM pass
euisuny/mafia-of-ocaml
euisuny/merge-macros
euisuny/metalib
The Penn Locally Nameless Metatheory Library
euisuny/nbe
euisuny/ocaml
The core OCaml system: compilers, runtime system, base libraries
euisuny/plclub-web-1
A Hakyll [plclub] website (https://www.cis.upenn.edu/~plclub/)