Dependent Type

Learning Dependent Types とても丁寧な入門記事

A Tutorial Implementation of a Dependently Typed Lambda Calculus LambdaPiというシンプルな依存型を備えたλ計算の拡張を書くチュートリアル

Elaboration

Type theory elaboration

dependently typed languagesの実装方法を解説してくれるビデオシリーズ Githubに実装も公開してある。

The Lean Theorem Prover (system description) Elaboration in Dependent Type Theory

Leanでの実装方法

Lecture Notes on Elaboration

smalltt

Demo for high-performance type theory elaboration

Linear Types inside Dependent Type Theory