| Conclusion |
|
|
|
|
|
|
| • | Designed
an explicit, transparent, and statically |
||||
| verifiable
language for staged computation |
|||||
| • | Conservative
over existing language(s) |
||||
| • | Tools
of logic and type theory are critical |
||||
