Licorne is an experimental programming language exploring refinement types and language-based support for lightweight verification.
The compiler supports parsing (although the parser is very basic), IR generation, type inference, and type-checking. It does not have a backend (yet).
Some features that are already supported:
- Dependent range types
- General refinement types
- Bidirectional type inference
- Kotlin-style smartcasts (including range types inference from branching conditions)
- Explicit method preconditions
- Kotlin-style nullable types
Code examples can be found in the test resources directory.
To build the compiler, run sbt assembly in the licorne-compiler directory.
To type-check a program using the (jar of the) compiler, run java -jar <jar-name> compile src_file.lic (or java -jar <jar-name> compile src/* to compile all files in ./src).
SMT solver integration: the compiler uses Z3 via the KSMT API.
Notes on naming: Licorne stands for "Language-level InferenCe Of RefiNEments", and means "unicorn" in French. Earlier versions of Licorne were called Rattlesnake and Grattlesnake, the former being a very simple toy language, and the latter corresponding to my master's thesis work on gradual object capabilities. They can be found on other branches of this repository.