Repository navigation

thesis

Public

About

Compiling Concurrency Correctly—Verifying Software Transactional Memory

agda concurrency formal-proofs proof proof-assistant software-transactional-memory thesis

5 stars

1 watching

Report repository

Name		Name	Last commit message	Last commit date
Atomic		Atomic
Fork		Fork
NonDet		NonDet
Verified		Verified
.gitignore		.gitignore
Bookshelf.bib		Bookshelf.bib
Common.agda		Common.agda
Makefile		Makefile
README.md		README.md
agda.fmt		agda.fmt
agda.lagda		agda.lagda
atomic.lagda		atomic.lagda
conclusion.tex		conclusion.tex
deelite.sed		deelite.sed
fork.lagda		fork.lagda
haskell.fmt		haskell.fmt
introduction.lhs		introduction.lhs
latex.mk		latex.mk
lhs2TeX.mk		lhs2TeX.mk
model.lhs		model.lhs
nondet.lagda		nondet.lagda
polycode.lhs		polycode.lhs
semantics.tex		semantics.tex
stm.lhs		stm.lhs
testing.lhs		testing.lhs
thesis.tex		thesis.tex
verified.lagda		verified.lagda
wordcount.wc		wordcount.wc

Repository files navigation

Compiling Concurrency Correctly

Verifying Software Transactional Memory

Nottingham eTheses —final published PDF

“Compiling Concurrency Correctly—Verifying Software Transactional Memory” by Liyang HU is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

About

Compiling Concurrency Correctly—Verifying Software Transactional Memory

agda concurrency formal-proofs proof proof-assistant software-transactional-memory thesis

5 stars

1 watching

Report repository

Releases

Packages

Used by

Contributors

Languages