Data

Tools

Indexes

Applications

Experiments

Open Source Science

fyp

Final year project

https://github.com/nathanielb123/fyp

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (5.5%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Final year project

Basic Info
  • Host: GitHub
  • Owner: NathanielB123
  • Language: Agda
  • Default Branch: main
  • Size: 4.45 MB
Statistics
  • Stars: 10
  • Watchers: 1
  • Forks: 1
  • Open Issues: 0
  • Releases: 0
Created over 1 year ago · Last pushed 8 months ago
Metadata Files
Readme Citation

README.md

Bits and Pieces Relating to my Final Year (Masters) Project at Imperial: Local Rewriting in Dependent Type Theory

Guide:

  • submitted.pdf: The submitted final report.
  • slides.pdf: Presentation slides. I have also uploaded a recording of the live presentation to YouTube.
  • Dependent: Agda mechanisations of a minimal dependent type theory with Booleans, and the extended languages "SCBool" and "SCDef", as defined in the report.
  • Check: A bidirectional NbE typechecker for "SCBool".
  • Untyped: A proof that for untyped lambda calculus with Booleans, well-foundedness of "non-deterministic reduction" (as defined in the report) implies well-foundedness of "spontaneous reduction" (again as defined in the report, basically β-reduction plus arbitrary rewrites to closed Booleans).
  • STLC: A proof that STLC is strongly normalising w.r.t. spontaneous reduction, based on András Kovács' StrongNorm.agda (which itself is based on Girard's SN proof for STLC in "Proofs and Types"). In the report, instead of proving SN of spontaneous reduction directly (which gets a bit convoluted), we prove SN w.r.t. non-deterministic reduction.
  • Completion.hs: (Very naive) implementations of ground completion and E-Graphs for first order terms, just to learn the concepts.
  • Report: LaTeX/literate Agda source for the interim/final reports and presentation slides.

Note:

Some of the Agda mechanisations (specifically the "strictified" syntaxes in the Dependent folder, and any files that depend on them) require my fork of Agda to typecheck (specifically, the mutual-rewrite branch pushed here).

Owner

  • Name: Nathaniel Burke
  • Login: NathanielB123
  • Kind: user

Citation (CITATION.bib) 

@thesis{burke2025local,
  title={Local Rewriting in Dependent Type Theory},
  author={Burke, Nathaniel},
  year={2025},
  url={https://github.com/NathanielB123/fyp/blob/main/submitted.pdf},
  type={mathesis},
  school={Imperial College London},
}

GitHub Events

Total
  • Watch event: 6
  • Issue comment event: 1
  • Push event: 120
  • Pull request event: 2
  • Fork event: 1
  • Create event: 1
Last Year
  • Watch event: 6
  • Issue comment event: 1
  • Push event: 120
  • Pull request event: 2
  • Fork event: 1
  • Create event: 1