Email Gateway (Jul 20 2022 at 19:00): Email Gateway (Jul 20 2022 at 19:00):From: Joe Wells <cl-isabelle-users@lists.cam.ac.uk>
dear experts in writing academic papers connected to isabelle,
a reviewer of a paper using somewhat isabelle-inspired syntax complained
about too much “type theory slang” that “makes it very hard for someone
not deeply in that world”. (i think this reviewer has likely not been
asked to review papers on homotopy type theory.)
we promised this reviewer that we would make various changes and they
graciously raised their -2 reject to a 0 neutral and our paper was
accepted on the strength of the other reviews.
one of the changes we promised was that we would attempt to include
better explanations of higher-order abstract syntax.
are there any papers that explain this aspect of isabelle in a way that
you find particularly good? we would like to see how they do it. can
you recommend good examples? ideally short papers, as we only have 16
pages lncs format.
thanks for any advice you can give.
best wishes,
joe
Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:
1. Heriot-Watt University, a Scottish charity registered under number SC000278
2. Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.
The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.
Email Gateway (Jul 20 2022 at 19:13):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
I don't know what your paper is about and what "type theory slang" it
contains. I don't think anyone needs to know a lot of type theory to
understand applications of Isabelle; papers about Isabelle itself
may be another matter (albeit still fairly simple compared to, as you
rightly said, something like Homotopy Type Theory). But then one would
be justified in saying that the reader of such a paper can be expected
to know a bit about types.
Well, it's hard to say without knowing the context of that remark. But I
for one have never gotten such complaints even in non-theorem-proving
venues like ISSAC. Perhaps you just had bad luck with your reviewer?
Anyway, regarding your question: could you explain what you mean by
"higher-order abstract syntax" in the context of Isabelle? Are you
talking about the way terms are represented in Isabelle internally?
Manuel
Email Gateway (Jul 20 2022 at 19:23):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Either you run into the wrong reviewer or you submitted to the wrong
conference, but I am not going to debate about that.
Please feel free to check Isabelle papers published in ITP.
I ran into similar situations when I publish in certain communities that
are supposed to be Formal Methods communities, however they have a hard
time to understand what Isabelle actually is.
They think that the executable document model that Isabelle offers, and its
extenstion to a proof document for higher order logic (Isabelle/HOL), is
just a kind of source code and should not appear in the paper.
I hope one day they understand what ISAR is, and that Isabelle offers a
universal notation for logic when implemented on a machine, and it follows
mike gordon book introduction to HOL to some extent.
But I will not spend my time convincing “formal methods” communities to
understand that.
What I usually try to do is to translate what I have to a text book like
notations,eg., relational notations and a like.
Best wishes,
Yakoub.
Email Gateway (Jul 20 2022 at 19:38):From: Tobias Nipkow <nipkow@in.tum.de>
The use of higher-order abstract syntax, i.e. lambda terms, to express variable
binding operators is absolutely standard and Isabelle is just one of many
systems that employ this technique. Essentially, the idea goes back to Church:
in his 1932 paper on lambda calculus he introduces constants for existential and
universal quantifiers that take functions as arguments. The idea was (first?)
implemented in Automath. The name probably goes back to Frank Pfenning's highly
influential eponymous paper.
I am sure you are well aware of all of this. The idea of higher-order abstract
syntax is really quite basic, once you understand lambda calculus, and I don't
see that you need a lot of space to explain it. Most certainly there is nothing
special about Isabelle in this respect - except that Larry was one of the first
people to implement higher order unification as a means for automating
deductions involving lamda the terms.
Tobias
smime.p7s
Email Gateway (Jul 20 2022 at 19:49):From: Joe Wells <cl-isabelle-users@lists.cam.ac.uk>
yes, exactly.
i am wondering if there is a standard chunk of text (2 or 3 sentences,
perhaps a displayed formula or 2) that can be given (with some
variation) to help mathematicians read this stuff.
of course, i can write such explanations, but i was wondering if there
were two or three papers that people thought did an especially good job
of it.
thanks for any examples any of you can point me toward.
best wishes
joe
Email Gateway (Jul 20 2022 at 19:57):From: "John F. Hughes" <jfh@cs.brown.edu>
Let me echo Manuel's remark: "[ways to] help mathematicians read *this
stuff*" would be much easier to provide if you'd tell us explicitly, by at
least 2 or 3 examples, exactly what "this stuff" is. Go ahead and paste in
a paragraph of the paper you wrote! Please!
Last updated: Apr 20 2024 at 04:19 UTC