Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-10306
For citation please use:
Main Title: A Formalization of Typed Aspects for the ς-calculus in Isabelle/HOL
Author(s): Kammüller, Florian
Sudhof, Henry
Type: Research Paper
Language Code: en
Abstract: In this paper we present an approach towards safe software composition based on aspect-orientation. Aspects enable the systematic addition of code into existing programs but often they also introduce errors. In order to provide safe aspects for software composition we address the verification of the aspect-oriented language paradigm. We construct a basic calculus for aspects with types and prove formally type safety. More precisely, this paper presents the following contributions (a) a fully formalized type system for the Theory of Objects including the proof of type safety, (b) a theory of aspects based on the Theory of Objects including a type system for aspects, and (c) the definition of a notion of type safety for aspects including its proof. The entire theory and proofs are carried out in the theorem prover Isabelle/HOL.
URI: https://depositonce.tu-berlin.de/handle/11303/11422
http://dx.doi.org/10.14279/depositonce-10306
Issue Date: 2007
Date Available: 17-Jun-2020
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): type safety
aspect-orientation
safe software composition
verification
language
type system
License: http://rightsstatements.org/vocab/InC/1.0/
Series: Forschungsberichte der Fakultät IV - Elektrotechnik und Informatik / Technische Universität Berlin
Series Number: 2007-20
ISSN: 1436-9915
Appears in Collections:Fak. 4 Elektrotechnik und Informatik » Publications

Files in This Item:
tr-2007-20.pdf
Format: Adobe PDF | Size: 307.97 kB
DownloadShow Preview
Thumbnail

Item Export Bar

Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.