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:


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