gabriel-fallen / bidirectional-demo Public

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

A demo implementation of a simple bidirectional type-checker in Lean 4.

9 stars 0 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 4 Commits
.gitignore		.gitignore
BidirDemo.lean		BidirDemo.lean
Main.lean		Main.lean
README.md		README.md
lakefile.lean		lakefile.lean

Repository files navigation

Bidirectional Type-Checking

A demo implementation of a simple bidirectional type-checker (for STLC) in Lean 4.

Resources

Presentation recording: https://www.youtube.com/watch?v=BL-OXeTtw1g

Slides: https://drive.google.com/file/d/1qAx97cydrJ6qP8dCV5wrivXamKXLyGfD/view?usp=sharing

Literature

Pfenning, Frank (2004). Lecture notes for 15-312: Foundations of Programming Languages

Christiansen, D. R. (2013). Bidirectional typing rules: A tutorial

Dunfield, J., & Krishnaswami, N. (2021). Bidirectional typing. ACM Computing Surveys (CSUR), 54(5), 1-38

About

A demo implementation of a simple bidirectional type-checker in Lean 4.

bidirectional type-checking lean4

Report repository

Languages

Lean 100.0%