juniorxxue / system-f Public

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

System F in Agda with well-scoped de Bruijn indices

0 stars 0 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
Main.agda		Main.agda
Prelude.agda		Prelude.agda
README.md		README.md

Repository files navigation

System F in Agda using well-scoped de Bruijn indices

Terms, Types and Contexts are well-scoped.

References

POPLMark: https://www.seas.upenn.edu/~plclub/poplmark/
alan-j-hu/STLC: https://github.com/alan-j-hu/STLC
sstucki/system-f-agda: https://github.com/sstucki/system-f-agda
Jesper's 1001 Representations of Syntax with Binding: https://jesper.sikanda.be/posts/1001-syntax-representations.html
Lysxia/system-F: https://github.com/Lysxia/system-F

About

System F in Agda with well-scoped de Bruijn indices

agda debruijn-indices systemf

Report repository

Languages

Agda 100.0%