This repository has been archived by the owner on Sep 5, 2023. It is now read-only.

intsuc / lambda_d Public archive

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

An experimental implementation of a dependently typed language in Kotlin

4 stars 1 fork Branches Tags Activity

Notifications

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.

About

An experimental implementation of a dependently typed language in Kotlin

dependent-types

Report repository

Releases

No releases published

Packages

No packages published

Contributors 2

Languages

Kotlin 100.0%