Student Project: An Isabelle Formalization of the Universe Type System
Download: PDF.
“An Isabelle Formalization of the Universe Type System” by Martin Klebermaß. Apr. 2007. Master's thesis, co-supervised with Prof. T. Nipkow, T. U. München.
Abstract
Today still very often faulty software is delivered. In contrast to other engineering tasks no one wonders about that. But there are a lot of areas where faulty software could generate high costs.
To solve that problem the correctness of software should be guaranteed.
The Universe Type System helps to make this step more simple. It allows to structure the heap memory into contexts. Those contexts can be used to reason about software.
As the type system will be used to prove the correctness of programs, the type system itself has to be shown sound.
The goal of this diploma thesis is to formalize the Universe Type System using a Featherweight Java like syntax, extended with field updates. The formalization will be proved using the theorem prover Isabelle/HOL. It is based on the Isabelle/HOL Featherweight Java Implementation, the paper about generic universe types and the Universe Java paper. The proof is separated into a proof of preserving the topology, and a proof of the encapsulation of the type system.
Using Isabelle/HOL, it was possible to show the type preservation of the semantics, as well as the owner as modifier property. Also a new interpretation of the universe modifiers for arrays has been shown sound.
Download: PDF.
BibTeX entry:
@unpublished{MKlebermass07,
author = {Martin Kleberma{ss}},
title = {{An Isabelle Formalization of the Universe Type System}},
month = apr,
note = {Master's thesis, co-supervised with Prof. T. Nipkow, T. U.
M{"u}nchen}
}
Back to the student projects sorted by date or by category.
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
(This webpage was created with bibtex2web.)