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



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.

Such a long sequence appeared in early versions of my Monomorphic_Monad formalisation in the AFP. (There was a record for a monad, an extension for exceptions, another one for state, etc.) But I dropped the whole record approach because the fixed order of record extensions made the whole approach too inflexible. Today, Monomorphic_Monad is based on locales.

All my records are small in terms of fields and I have frequently used extensions, but usually no deeper than three levels. Some examples can be found in the unfinished FSCPI formalisation at:

https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/projects/FCSPI/CoSP.zip

Andreas




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