Email Gateway (Aug 22 2022 at 15:37): Email Gateway (Aug 22 2022 at 15:37):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
nice!
When I read these announcements, I always wonder: Is this a
formalization of some theory that just stand there on its own, in order
to be marveled at (and pointed at if people have abouts about the
proofs in a corresponding paper verison)? Or is this a library, to be
used as a tool in unrelated developments?
Clearly, AFP is home for both kind of entries. The containers framework
is clearly the latter part; Gödel’s inconsistency arguably the former.
Would it be feasible to mark entries in the AFP that are intended to be
used as libraries explicitly? So that whenever I find the standard
library lacking, I have a much shorter list to go through?
Greetings,
Joachim
(who has to do Coq these days, and would love to have at least the
equivalent of Isabelle’s standard library around…)
signature.asc
Email Gateway (Aug 22 2022 at 15:38):From: Makarius <makarius@sketis.net>
When you have become a proven expert of both Coq and Isabelle it would
be nice to see some report or paper comparing both worlds to the ITP
community.
It is important to exchange the best ideas in order to make real progress.
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 15:39):From: Lawrence Paulson <lp15@cam.ac.uk>
Agree 100%!
Larry
Email Gateway (Aug 22 2022 at 15:39):From: Tobias Nipkow <nipkow@in.tum.de>
On 01/06/2017 16:54, Joachim Breitner wrote:
Hi,
nice!
When I read these announcements, I always wonder: Is this a
formalization of some theory that just stand there on its own, in order
to be marveled at (and pointed at if people have abouts about the
proofs in a corresponding paper verison)? Or is this a library, to be
used as a tool in unrelated developments?Clearly, AFP is home for both kind of entries. The containers framework
is clearly the latter part; Gödel’s inconsistency arguably the former.Would it be feasible to mark entries in the AFP that are intended to be
used as libraries explicitly? So that whenever I find the standard
library lacking, I have a much shorter list to go through?
On the technical side it is easy enough to add another field to each submission,
but then the interface would also need to support specific views of the AFP.
This means work is required to design and implement the idea. Maybe it will
happen as part of Larry's ERC project?
Moreover it is not always a clear cut decision into which category an entry
falls. It may have a library component plus some application.
For the time being, consider the need to look closely a blessing in disguise:
that way you get to know the AFP better ;-)
Tobias
Greetings,
Joachim
(who has to do Coq these days, and would love to have at least the
equivalent of Isabelle’s standard library around…)
Last updated: Nov 21 2024 at 12:39 UTC