2020-05-28 13:48:51 (GMT)
Let's make suggestions and vote!
2020-05-28 13:51:16 (GMT)
I'd like something more ITP/ATP oriented, maybe. Something about mizar and hammers?
2020-05-28 13:52:14 (GMT)
Which of the 2 zillion papers by Josef Urban are you thinking of? ;)
2020-05-28 13:53:17 (GMT)
would a survey paper do?
2020-05-28 13:53:32 (GMT)
Maybe
Chad E. Brown, Josef Urban
Extracting Higher-Order Goals from the Mizar Mathematical Library
https://arxiv.org/pdf/1605.06996.pdf
?
2020-05-28 13:54:38 (GMT)
I will not be available before July 15th: exams, moving, taking care of my mother, and usual business will keep me busy. All the best
2020-05-28 13:54:38 (GMT)
There's a survey called "Hammering towards QED", but it has two flaws: It's very long and I'm a coauthor. (As a principle, I think we shouldn't read each others' papers as part of the reading club, but other people's.)
2020-05-28 13:55:54 (GMT)
Yeah, maybe not then.
2020-05-28 13:56:34 (GMT)
How about:
"Formalization of the fundamental group in untyped set theory using auto2"
Bohua Zhan
https://arxiv.org/abs/1707.04757
2020-05-28 13:57:59 (GMT)
I saw the talk. ;) It's very impressive work.
2020-05-28 13:58:55 (GMT)
There's also the first auto2 paper:
Bohua Zhan
AUTO2, a saturation-based heuristic prover for higher-order logic
ITP 2016
https://arxiv.org/pdf/1605.07577.pdf
2020-05-28 13:59:59 (GMT)
The first auto2 paper I also saw in Nancy :)
2020-05-28 14:2:58 (GMT)
I like the idea of trying something more ITP oriented. I suggest:
2020-05-28 14:2:59 (GMT)
A metaprogramming framework for formal verification
Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura
https://leanprover.github.io/papers/tactic.pdf
2020-05-29 9:37:25 (GMT)
Is it a typo in the title or is the next meeting really on Monday?