Skip to content

A dump of language and typing paper implementations, and my own experiments

License

Notifications You must be signed in to change notification settings

shua/lang-noodles

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

31 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Noodling around with programming language.

I'm going to dump any language experiments here.

mostly complete:
- strand.rs: minimal strand implementation http://www.call-with-current-continuation.org/strand/strand.html
- bidir_typeck.rs: https://arxiv.org/abs/1306.6032 "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism"
- ctl_star.rs: model checker for CTL* https://en.wikipedia.org/wiki/CTL*
- hottest_dep.rs: https://www.youtube.com/watch?v=DEj-_k2Nx6o "HoTTEST Summer School 2022: How to code your own Type Theory"
- ukanren.rs: micro-kanren http://minikanren.org/

incomplete:
- graphck: attempt to understand TLA+ by writing my own https://lamport.azurewebsites.net/tla/tla.html
- ecmtt.rs: https://arxiv.org/abs/1202.0904 "Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)"
- fomega.rs: system-f-omega https://en.wikipedia.org/wiki/System_F#System_F%CF%89
- fp2.rs: https://www.microsoft.com/en-us/research/uploads/prod/2023/05/fbip.pdf "FP²: Fully in-Place Functional Programming"

experiments:
- f_cap.rs: system-f but capabilities to limit availalable syntax
- l0612.rs: gradually typed assembly
- record.rs: every block is a record type, no need for 'let's, "|- {x=1, y=2, x} : {x:N, y:N, N}"
- spaced.rs: use spacing instead of parentheses "x + y  *  z" = "(x+y)*z"

About

A dump of language and typing paper implementations, and my own experiments

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published