5 ms·

And the scary thing is that one can do even better: https://billwadge.wordpress.com/2016/01/18/extensional-higher-order-prolog/ https://billwadge.wordpress.com/

And the scary thing is that one can do even better: https://billwadge.wordpress.com/2016/01/18/extensional-higher-order-prolog/ https://billwadge.wordpress.com/2016/01/18/extensional-highe... https://github.com/acharal/hopes https://github.com/acharal/hopes

agumonkey 10y ago
Ha nice, I was looking for recent advances in this branch; most of things went the CPL way.
nickpsecurity 10y ago
Neat tools. Have you seen any attempts to model HOL in FOL for verification in FOL? There's a FOL down to assembly verified prover and stack. It's ACL2-like. I also found a paper doing HOL-to-FOL conversion with that tool modeled and proven in HOL. Doing HOL in FOL or HOL-to-FOL converter in FOL seems like a short-cut to verified, proof stack. If the shortcut is doable at all. The HOL-to-FOL gave me some excitement about this. It just wasn't done entirely in FOL itself.
- tomcam 10y ago
  I understood none of that FOLdeROL
  - nickpsecurity 10y ago
    It was for an audience that would. The rest would be unlikely to be helpful. Filtering trick. ;) Anyway, here's the work the result will build on whose description is useful to wider audience: https://www.cs.utexas.edu/users/jared/milawa/Web/ https://www.cs.utexas.edu/users/jared/milawa/Web/ https://cakeml.org/ https://cakeml.org/
    - tomcam 10y ago
      Hey, pretty neat--thanks
- catnaroek 10y ago
  Haven't seen it, but I'll check it out. Thanks for the pointer.
  - nickpsecurity 10y ago
    Forgot to add the link so you can see what such a process might look like. Here's slides and a paper on one that merged HOL and ACL2. But it verified that in HOL4, not ACL2. https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD06/presentations/FMCAD-2006-Wednesday/Session2-Hunt.pdf https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD06/presentations/... http://www.ccs.neu.edu/home/pete/acl206/papers/gordon.pdf http://www.ccs.neu.edu/home/pete/acl206/papers/gordon.pdf
deleted 10y ago
[deleted]

agumonkey 10y ago

Ha nice, I was looking for recent advances in this branch; most of things went the CPL way.

nickpsecurity 10y ago

Neat tools. Have you seen any attempts to model HOL in FOL for verification in FOL? There's a FOL down to assembly verified prover and stack. It's ACL2-like. I also found a paper doing HOL-to-FOL conversion with that tool modeled and proven in HOL. Doing HOL in FOL or HOL-to-FOL converter in FOL seems like a short-cut to verified, proof stack. If the shortcut is doable at all. The HOL-to-FOL gave me some excitement about this. It just wasn't done entirely in FOL itself.

tomcam 10y ago
I understood none of that FOLdeROL
- nickpsecurity 10y ago
  It was for an audience that would. The rest would be unlikely to be helpful. Filtering trick. ;) Anyway, here's the work the result will build on whose description is useful to wider audience: https://www.cs.utexas.edu/users/jared/milawa/Web/ https://www.cs.utexas.edu/users/jared/milawa/Web/ https://cakeml.org/ https://cakeml.org/
  - tomcam 10y ago
    Hey, pretty neat--thanks
catnaroek 10y ago
Haven't seen it, but I'll check it out. Thanks for the pointer.
- nickpsecurity 10y ago
  Forgot to add the link so you can see what such a process might look like. Here's slides and a paper on one that merged HOL and ACL2. But it verified that in HOL4, not ACL2. https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD06/presentations/FMCAD-2006-Wednesday/Session2-Hunt.pdf https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD06/presentations/... http://www.ccs.neu.edu/home/pete/acl206/papers/gordon.pdf http://www.ccs.neu.edu/home/pete/acl206/papers/gordon.pdf

deleted 10y ago

[deleted]