Re: [isabelle] Proof of concept: BNF-based records



(re-sending, as I first used a non-subscribed email address)

Hi,
>  I dimly remember that Andeas Lochbihler had an application of a
> long sequence of record extensions (depth 5 or 6), but can not find
> the corresponding formalization in Isabelle+AFP.

We are currently porting (at this point in time, manually) the
extensible encoding for class model from my PhD thesis [A] to
records. Our main application at the moment is a formalization of the
Document Object Model (DOM) and partly HTML (as an extension of the
DOM) for reasoning over browser APIs that modify DOM/HTML instances
(a first AFP submission is planned for the near future).

Here, we easily end up with 5 and more extensions and also rather
complex type polynoms as extension types. 

We moved from a datatype-based approach to record to benefit from the
records syntax and also to re-use the existing extensibility of records
(instead of implementing our own using records or tuples as we did in
our old object-oriented datatype package). 

Best,
        Achim

[A] Achim D. Brucker, Burkhart Wolff: An Extensible Encoding of
    Object-oriented Data Models in hol. J. Autom. Reasoning 41(3-4):
    219-249 (2008)
    https://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b
-- 
Dr. Achim D. Brucker | Software Assurance & Security | University of Sheffield
               https://www.brucker.ch | https://logicalhacking.com/blog
                           @adbrucker | @logicalhacking 

Attachment: signature.asc
Description: PGP signature



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