3 ms·
There's been some interesting work by Conor McBride on Epigram where he uses structural editing to help communicate the proof burdens that the compiler can infe
by tel 13y ago
There's been some interesting work by Conor McBride on Epigram where he uses structural editing to help communicate the proof burdens that the compiler can infer and what remains for the user to do. Epigram is long gone, but there are still papers describing how it worked.
- seanmcdirmid 13y agoAlso, Elliott's Tangible Functional Programming: http://conal.net/papers/Eros/ http://conal.net/papers/Eros/