stlc_debruijn
Simply Typed Lambda Calculus with de Bruijn indices
Science Score: 54.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
-
✓Committers with academic emails
1 of 2 committers (50.0%) from academic institutions -
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (3.0%) to scientific vocabulary
Repository
Simply Typed Lambda Calculus with de Bruijn indices
Basic Info
- Host: GitHub
- Owner: ElifUskuplu
- License: mit
- Language: C
- Default Branch: main
- Homepage: https://elifuskuplu.github.io/Stlc_deBruijn/
- Size: 4.81 MB
Statistics
- Stars: 14
- Watchers: 2
- Forks: 0
- Open Issues: 0
- Releases: 0
Metadata Files
README.md
STLC with de Bruijn in Lean4
Simply Typed Lambda Calculus with de Bruijn indices in Lean4
The project is based on the paper "The Locally Nameless Representation" by Arthur Chargu´eraud. I mostly used his Coq library when I formalize the definitions in Lean4.
The two important parts of the library are: 1) We formalized the proof of confluence of the beta reduction in locally nameless syntax. 2) (Novel part) We proved and formalized that the beta reduction in locally nameless syntax is strongly normalizing.
Note: This work is a continuation of our project conducted in the Formalization of Mathematics (SLMATH) summer program, suggested by Jeremy Avigad.
To use the library, Lean4 and mathlib library should be installed.
Owner
- Login: ElifUskuplu
- Kind: user
- Repositories: 2
- Profile: https://github.com/ElifUskuplu
Citation (CITATION.cff)
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: Elif
given-names: Uskuplu
orcid: https://orcid.org/0000-0003-3836-7193
title: "Simply Typed Lambda Calculus with de Bruijn indices in Lean4"
GitHub Events
Total
- Watch event: 8
- Push event: 34
Last Year
- Watch event: 8
- Push event: 34
Committers
Last synced: 10 months ago
Top Committers
| Name | Commits | |
|---|---|---|
| ElifUskuplu | e****u@u****u | 38 |
| ElifUskuplu | 7****u | 16 |
Committer Domains (Top 20 + Academic)
Issues and Pull Requests
Last synced: 10 months ago
All Time
- Total issues: 0
- Total pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Total issue authors: 0
- Total pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0