Re: [isabelle] Clone detection for Isabelle theories



On 07/13/2016 04:16 PM, Lars Hupel wrote:

> I'd like to announce the availability of a technology preview of code
> clone detection for Isabelle theories.

Interesting.

As far as I understood from the paper,
you are parsing source code with libisabelle,
which in turn requires a full Isabelle installation.
(Then - is parsing safe? Or is there danger of
code injection?)

I'd hope there is something like Language.Isabelle,
(just AST data type and parser - no semantics). cf.
https://hackage.haskell.org/package/haskell-src-exts
https://hackage.haskell.org/package/language-javascript

very hypothetically - is there a formal Isabelle(Isar) grammar
from which AST representation and parser/printer (in Haskell)
could be generated (mostly) automatically?

Best regards, J. Waldmann.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.