Abstract

Reasoning about computers and programming languages on paper is most often done with set theory, while most proof assistant formalizations of languages and programs use alternative mathematical foundations. One of the few exceptions has been Mizar where the Simple Concrete Model of computers has been used to verify programs expressed as abstract programming language instruction sequences. The model uses extended set theory features including structures and Fraenkel set comprehension operators. In this paper we show how to formally specify such objects in the Isabelle object logic implementing the Mizar foundations as definitional extensions. To show the adequacy and usability of the mechanisms, we reformalize a number of Mizar definitions and theorems related to structures and set comprehensions, including both mathematical and programming language examples: groups, machines and properties of computer memory states.

BibTeX

@inproceedings{ckkp-macis17,
  author    = {Cezary Kaliszyk and Karol Pak},
  title     = {Isabelle Formalization of Set Theoretic Structures and Set Comprehensions},
  pages     = {163--178},
  doi       = {10.1007/978-3-319-72453-9_12},
  booktitle = {International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017)},
  year      = {2017},
  editor    = {Blömer J. and Kotsireas I. and Kutsia T. and Simos D.},
  series    = {LNCS},
  volume    = {10693},
  publisher = {Springer},
}