cur
cur copied to clipboard
wilbowma
A less devious proof assistant
If the point of Cur is notation, then infix syntax is important. Parsing s-expressions is easy for computers, but humans are quite good at parsing mixfix notation. It can be...
https://ncatlab.org/nlab/show/Globular https://golem.ph.utexas.edu/category/2015/12/globular.html
Using the reflection API can result in quadratic(i think) type-checking/expansion
Right now, modules are provided partly by wrapping Racket modules and partly by a giant ball of hacks. I wonder if we could gain first-class modules, something akin to ML...
"The core language of cur is essentially TT" add citation here. The citation is in the first paragraph udner "Curnel Forms", but should also be on the main page.
Figure out how to interoperate w/ Coq, Agda, etc. Being able to important other prover's libraries would be handy.
Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors (CHI 2015) with Stephen R. Foster and William G. Griswold http://cseweb.ucsd.edu/~lerner/pb.html Without more research, may only work for first-order theorems.
My understanding is that Coq's Fixpoint is just a complicated macro. This paper, http://www.chargueraud.org/research/2009/fixwf/fixwf.pdf, suggests is should be simple to implement. See if we can implement this in Cur, in...
The `cur-normalize` form provided by the reflection API enables staged meta-programming. However, currently it relies on whatever normalization strategy is employed in the Curnel. The user may want more or...