Pinned Repositories
CompCert
The CompCert formally-verified C compiler
CompCertMod
A version of CompCompcert compatible with coq8.6 and with the Concurrent Permission Machine.
COS424
COS424
COS510
Programming Languages class
emacs.d
Emacs initialization files
Emacs_configure
Tips for setting up my Emacs
fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
histogram
A Haskell package for easily creating histograms
MemoryModelVerification
Specifying Microarchitectural Memory Consistency Models for Verification in PipeCheck
scuellar's Repositories
scuellar/MemoryModelVerification
Specifying Microarchitectural Memory Consistency Models for Verification in PipeCheck
scuellar/CompCertMod
A version of CompCompcert compatible with coq8.6 and with the Concurrent Permission Machine.
scuellar/CompCert
The CompCert formally-verified C compiler
scuellar/COS424
COS424
scuellar/COS510
Programming Languages class
scuellar/emacs.d
Emacs initialization files
scuellar/Emacs_configure
Tips for setting up my Emacs
scuellar/fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
scuellar/histogram
A Haskell package for easily creating histograms
scuellar/MMap
MMap coq project OPLSS
scuellar/MicroRAM
Exploratory project to understand tinyRAM
scuellar/narcissus_errors
Adding user-friendly errors for encoders and decoders to Narcissus
scuellar/NewCompCert
scuellar/parsec
A monadic parser combinator library
scuellar/pawnshop
Opening practice at your own level
scuellar/puthesis
the thesis
scuellar/python-lichess
Python client for the lichess.org API (Now with Opening Explorer access)
scuellar/Python-programming-exercises
100+ Python challenging programming exercises
scuellar/racer
Rust Code Completion utility
scuellar/saw-script
The SAW scripting language.
scuellar/SMT_VST
scuellar/SoundVerifier
Automatic verifier proven sound all the way down to machine language
scuellar/thesis
Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency.
scuellar/thesis_pdf
Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency.