[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

Jesse:

>This may be somewhat inappropriate for mizar-forum, but it seems
>noteworthy to me that in the non-exhaustive list of systems for
>dependent types mentioned in this recent post to the TYPES forum, mizar
>is not mentioned.  Would it be appropriate to write an article on
>mizar's dependent types for the upcoming special issue of Fundamenta
>Informaticae?  One initial question to consider: does mizar's type
>system differ in any interesting way from the type sytems mentioned
>below?

The answer to your last question is undoubtedly "yes!"

Note however that this is about depedently typed
_programming,_ while the Mizar language is not a programming
language at all.  At least, there is no execution model
for Mizar expressions that I am aware of.

Freek