kirraObj-s-archives / lambda_d Public

forked from intsuc/lambda_d

Notifications You must be signed in to change notification settings
Fork 0
Star 0

An experimental implementation of a dependently typed language in Kotlin

0 stars 1 fork Branches Tags Activity

Name		Name	Last commit message	Last commit date
Latest commit History 66 Commits
.github		.github
gradle/wrapper		gradle/wrapper
src		src
.gitattributes		.gitattributes
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md
build.gradle.kts		build.gradle.kts
gradle.properties		gradle.properties
gradlew		gradlew
gradlew.bat		gradlew.bat
settings.gradle.kts		settings.gradle.kts

Repository files navigation

$\lambda_d$

An experimental implementation of a dependently typed language $\lambda_d$ in Kotlin

Features

Type in type
de Bruijn indices/levels
Type-preserving compilation
Patterns

References

AndrasKovacs/elaboration-zoo
jozefg/nbe-for-mltt
András Kovács. Type theory elaboration 1: bidirectional type checking
András Kovács. Type theory elaboration 8: comparison of De Bruijn, non-shadowing and fresh variable conventions
Jon Sterling. Jon Sterling, How to code your own type theory
Dunfield, J., & Krishnaswami, N.R. (2019). Bidirectional Typing. ACM Computing Surveys (CSUR), 54, 1 - 38.