Giter Club home page Giter Club logo

l1c's Introduction

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.

l1c's People

Contributors

j-baker avatar

Stargazers

Pialex99 avatar Amir M. Saeid avatar Ben Turrubiates avatar Matěj avatar Brendan Zabarauskas avatar timothy avatar Alex Gryzlov avatar avatar Gao Zhiyuan avatar Elliot Potts avatar Carter Tsai avatar Shih-Ying Allen Chen avatar sappy avatar HankWang avatar avatar Kuan-Yen Chou avatar swh avatar dboyliao avatar Yi-Hsiang Kao avatar EastL avatar hydai avatar Hsin-lin Cheng avatar avatar Angus H. avatar Federico Carrone avatar Matthew Markland avatar Andrei Dragomir avatar Suminda Sirinath Salpitikorala Dharmasena avatar Nicholas avatar Joshua Yanovski avatar Rex O. Amin avatar Bojan Čoka avatar avatar Conail Stewart avatar avatar Andrew Hodges avatar avatar Harold Ancell avatar avatar avatar Alec avatar Chucky Ellison avatar Chiu-Hsiang Hsu avatar Paulo Matos avatar Márk Bartos avatar Peter Clay avatar Nikolay Stoitsev avatar avatar Will Price avatar Nenad Rakocevic avatar avatar Erik Garrison avatar geppy avatar Garrett Barboza avatar Anatoly Chernov avatar

Watchers

avatar Ramana Kumar avatar James Cloos avatar Anatoly Chernov avatar avatar avatar avatar avatar

Forkers

eftychis aa10000 rbugoo131 dboyliao hongyunnchen shihyu knight-x cartertsai p-cpu

l1c's Issues

Write unit tests for the parser

I don't currently have plans to formally verify my parser. In this case, it seems smart to write some test programs, verify that they are parsed correctly by hand, and force correct compilation of these into the build progress.

Frontend

Take as input a file of concrete syntax, output assembly.

Write parser

Write a PEG based parser for the concrete L1 syntax

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.