Skip to content
/ l1c Public

l1c is a simple formally verified compiler for a while language

License

Notifications You must be signed in to change notification settings

j-baker/l1c

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

l1c: A simple verified toy compiler for a toy language

Build Status

This project was written for my University of Cambridge BA Computer Science Part II dissertation.

l1c is a verified compiler for the L1 language presented in the Cambridge Semantics of Programming Languages course.

The target language is a slight modification of the vsm0 VM presented in the Cambridge Compiler Construction course.

The operational semantics of these two languages can be found in:

The compiler is verified, meaning that there exists a proof that the compiler preserves the semantics of a program. The main correctness result can be found here.

The produced dissertation can be found in the dissertation directory. This repository is made available for illustration purposes; if you have a comprehension issue, feel free to file an issue.

Many thanks to Ramana Kumar and Magnus Myreen, who gave me important feedback over the course of the project.

About

l1c is a simple formally verified compiler for a while language

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages