GitHub - ziman/excomp: A certified compiler of exceptions from my thesis (Agda)

Name		Name	Last commit message	Last commit date
Latest commit History 40 Commits
.gitignore		.gitignore
Code.agda		Code.agda
Compiler.agda		Compiler.agda
Correctness.agda		Correctness.agda
Denotation.agda		Denotation.agda
Execution.agda		Execution.agda
Expression.agda		Expression.agda
README		README
TypeUniverse.agda		TypeUniverse.agda

Repository files navigation

Towards a verifiably correct compiler of expressions.
Loosely based on a paper by Graham Hutton: Compiling Exceptions Correctly

A certified compiler of exceptions from my thesis (Agda)