(The bootstrap compiler for) a dependently typed language with algebraic effects.
- Syntax
- Define
- Lexer
- Parser
- Core Language
- Define
- Typeck
- Codegen
- Prove progress
- Prove preservation
- Prove totality
- Prove codegen correctness
Licensed under either of
at your option.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.