Wow this was such an awesome viewing. I have found amazing work from the refinement typing folks at USCD. The book by Ranjit Dhalla is a gold mine! http://g

Wow this was such an awesome viewing. I have found amazing work from the refinement typing folks at USCD. The book by Ranjit Dhalla is a gold mine! http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf One question I had was can this be extended to type-drive "type" synthesis to derive new types and then use that to synthesize programs?