 |
Post AwBNApMqeFbeCKjuka by [email protected] |
 |
More posts by [email protected] |
|
Post #AwBNApMqeFbeCKjuka by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Proof assistant folks: what's the state of the art these days for extractin… |
|
|
|
Post #AwBNApWm3LXuh7NqDo by [email protected] |
|
0 likes, 1 repeats |
|
|
|
@lindsey Idris' compilation automatically uses an efficient representation … |
|
|
|
Post #AwBNAsJ3inMFJRzQlE by [email protected] |
|
0 likes, 1 repeats |
|
|
|
A bunch of folks are suggesting Lean, so let's see what Lean does for my Pe… |
|
|
|
Post #AwBNAsMbVcC3UReGHo by [email protected] |
|
0 likes, 0 repeats |
|
|
|
(This is -- for now -- leaving aside concerns about the large TCB of the extrac… |
|
|
|
Post #AwBxkvkQ07aklDHLiS by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey I think the thing with lean (at least lean 4) is that you're not s… |
|
|
|
Post #AwBxqji3ffbrA8wY1A by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@graydon Yeah, as @bentnib noted elsethread, the word "extraction" co… |
|
|
|
Post #AwBy01OpGoTUdINK0e by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey We haven't actually done this in the CertiCoq & VeriFFI projec… |
|
|
|
Post #AwBy021Sx9NoZ8SBEm by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey In other news, I'm working on extraction from Rocq to a mostly fun… |
|
|
|
Post #AwBy33G8oNEZGnl2Zc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bentnib @lindsey this is correct, from the Idris point of view at least. After… |
|
|
|
Post #AwBy33NaMhBldtEzB2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bentnib @lindsey I should add that the peano trick is built in, afaict. Idris… |
|
|
|
Post #AwBy33UfwKrNzsYeEC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jfdm @bentnib @lindsey Library design is crucial here, for not doing unary ari… |
|
|
|
Post #AwBy7noLfvHoo21Vi4 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jfdm @bentnib @lindsey it's looking at the type's shape after erasure … |
|
|
|
Post #AwByEMY7Qr8WHYYnQ0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey in Isabelle/HOL, you can do some special-casing yourself. Section 3:ht… |
|
|
|
Post #AwByOpNb63LQard3ce by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ah @lindsey and most of the types one'd want to use for programming that a… |
|
|
|
Post #AwByRy9Uw8vqfbX3Dc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey kyle, who's a friend, works on lean and is affiliated with ucsc an… |
|
|
|
Post #AwByRyHeRpSD4tLYvY by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@zmagg oh yeah, Kyle is great!! I had no idea you were friends! |
|
|
|
Post #AwBySvHL6dGG30ee8G by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bentnib well, now I want "agda2hs-to-coq" to exist, for no reason ot… |
|
|
|
Post #AwByb7c97tkWceIR5k by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@lindsey You'd hope that they'd be good Unix citizens and `cat my-cool-… |
