Pinned Repositories
beaglebone-ubuntu-scripts
Some scripts I use to maintain Ubuntu on the Beaglebone platform
best-resume-ever
:necktie: :briefcase: Build fast :rocket: and easy multiple beautiful resumes and create your best CV ever! Made with Vue and LESS.
c4
C in four functions
emesch
Classic Scheme to C. An exercise in Haskell
fo-mKanren-to-LF
Defunctionalized miniKanren with Universal Quantifier and Implication. Preprint: https://www.cs.toronto.edu/~lczhang/jin_universal2021.pdf
FPOP
Family Polymorphism for a proof assistant, an artifact. Paper : https://dl.acm.org/doi/10.1145/3591286
ITP.js
A Theorem Prover. Thanks to "Type Theory and Formal Proof" and flow.js.
ParaCDCL
Parametric CDCL Algorithm in Coq
Schmidty
Subtyping with sum type + Typed Scheme to LLVM. An exercise in Haskell.
tutorial-popl20
DKXXXL's Repositories
DKXXXL/FPOP
Family Polymorphism for a proof assistant, an artifact. Paper : https://dl.acm.org/doi/10.1145/3591286
DKXXXL/emesch
Classic Scheme to C. An exercise in Haskell
DKXXXL/fo-mKanren-to-LF
Defunctionalized miniKanren with Universal Quantifier and Implication. Preprint: https://www.cs.toronto.edu/~lczhang/jin_universal2021.pdf
DKXXXL/ITP.js
A Theorem Prover. Thanks to "Type Theory and Formal Proof" and flow.js.
DKXXXL/Schmidty
Subtyping with sum type + Typed Scheme to LLVM. An exercise in Haskell.
DKXXXL/tutorial-popl20
DKXXXL/best-resume-ever
:necktie: :briefcase: Build fast :rocket: and easy multiple beautiful resumes and create your best CV ever! Made with Vue and LESS.
DKXXXL/ParaCDCL
Parametric CDCL Algorithm in Coq
DKXXXL/VSchmidty
Semi-Verified Schmidty Interpreter. Soundness of Type system is proved. Trying to make it run on JS.
DKXXXL/checkedc
Contributions to Microsoft's Checked C project developed by PLUMmers
DKXXXL/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.
DKXXXL/coqfj
A mechanized proof of type safety for Featherweight Java using Coq
DKXXXL/dimsum-learning
DKXXXL/FullStackLearning
Full Stack Learning Experience
DKXXXL/FUSRP18-P6
DKXXXL/ixfree
DKXXXL/master-thesis
http://hdl.handle.net/10012/19531
DKXXXL/metaocaml-bibliography
MetaML and MetaOCaml bibliography
DKXXXL/MLFS.jl
MLFS type system: raising ML to the power of system F in a Simplest way
DKXXXL/parsimmon
A monadic LL(infinity) parser combinator library for javascript
DKXXXL/PLoTs2011
Imported from https://www.cs.purdue.edu/homes/bendy/PLoTs/index.html, including some personal note
DKXXXL/popl2018-papers
Link to preprints for POPL'18 and colocated events
DKXXXL/ppa-in-code
some my implementation of content in PPA
DKXXXL/resume
PDF Version:
DKXXXL/SoftwareFoundations-AfterCh15
Code Exercises after Ch15, from "Software Foundations"
DKXXXL/UTLCWSE
Many trivial languages interpreters. A Practice Area to verify them. Thanks to Software Foundations.
DKXXXL/VEmeschc
Semi-Verified Emesch Compiler, in Coq, in develop
DKXXXL/WasmCert-Coq
DKXXXL/webBug
A web crawler. An exercise on monad.
DKXXXL/webBug.backup
a web crawler.