This repository was archived by the owner on Jun 1, 2022. It is now read-only.
This repository was archived by the owner on Jun 1, 2022. It is now read-only.
Refinement types #16
Description
[type_pattern | predicate, predicate, ...]
# example
[x: Number | x > 0]
GreaterThan = (T, x: T) [y: T | y > x]
[(a: Type, Type) | a > 0, a < 10]
A type pattern is any type that may include x ~ Type.
Use Z3 as SMT solver.
Resources
https://en.wikipedia.org/wiki/Hoare_logic
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation
http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
http://strictlypositive.org/Easy.pdf
http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
Caveats
We need to ensure that pattern matching on refined types is exhaustive.