Pinned Repositories
cakeml
CakeML: A Verified Implementation of ML
HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
ace-jump-mode
a quick cursor jump mode for emacs
CFL-HOL
Theory of Context-Free Languages in HOL
Cplusplus
My C++ in HOL semantics
gorilla
Password Gorilla manages passwords
inspector-strategies
Verification of Inspector-style Compilations
JSON-SML
JSON parsing in SML (from SML/NJ's svn repo)
ordinals-paper
About mechanisations of the ordinals in higher order logic
Tasks
mn200's Repositories
mn200/CFL-HOL
Theory of Context-Free Languages in HOL
mn200/JSON-SML
JSON parsing in SML (from SML/NJ's svn repo)
mn200/inspector-strategies
Verification of Inspector-style Compilations
mn200/ace-jump-mode
a quick cursor jump mode for emacs
mn200/Cplusplus
My C++ in HOL semantics
mn200/gorilla
Password Gorilla manages passwords
mn200/ordinals-paper
About mechanisations of the ordinals in higher order logic
mn200/Tasks
mn200/bib2sx
A tool for manipulating bibtex files as s-expressions
mn200/concurrent-gc-verification
mn200/fxp
Validating XML parser library in Standard ML by Andreas Neumann and Alexandru Berlea
mn200/fxp145
Port of fxp1.4.5
mn200/itp_paper_07
Material to accompany submitted paper 7 to ITP2022
mn200/l4v
seL4 specification and proofs
mn200/mosml
Moscow ML is a light-weight implementation of Standard ML (SML), a strict functional language widely used in teaching and research.
mn200/netsem
Network Semantics
mn200/planning
PhD_project_1
mn200/polyml
Poly/ML