michaelsproul/honours-thesis

4th Year Honours Thesis on Programming Language Semantics

Honours Stuff

• Papers and summaries of papers.
• Books.
• Links to webpages/books (no need to store them, there's always archive.org). Discussions of links.
• Code and proofs.
• Slides and talks.
• Papers and literature reviews I've written.

Layout:

• Papers
• Books
• Links.md (file)
• Code
• Presentations
• Thesis

honours-thesis's Issues

Finish typing up L3's operational semantics

Restructure to put Progress and Preservation up front

Add typing rules for LLC and L^3.

Explanation of how they work, differences.

Finish typing up L3's typing rules

Evaluate proof automation

Argue the generality of the library with reference to DILL and L^3

Description of DILL may need to go in an earlier section.

Sweep over lit review, add Conor's Linear Dependent Types work

Describe high-level goals for the library (evaluation criteria)

Assess Coq proof quality according to eval framework

Finish discussing substitution lemmas

Write some framing stuff for the Own Work chapter

Check the Own Work chapter for mistakes and omissions

Update all Coq code examples

Finish explaining L3

Abstract

Finalise section about insert and context split

Talk about C

Outline odd CompCert behaviour.

Conclusion

Do a read-through from start to finish

Edit the section on variable naming