TACL Seminar Spring '03
From CSWiki
Spring '03 Schedule
Date | Speaker | Title | Links |
---|---|---|---|
Feb 24 | Amal Ahmed | Reasoning about Hierarchical Storage | Abstract |
Mar 24 | Koji Hasebe - Keito Univ | A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic | Abstract |
Abstracts
Amal Ahmed
Reasoning about Hierarchical Storage
In this paper, we develop a new substructural logic that can encode invariants necessary for reasoning about hierarchical storage. We show how the logic can be used to describe the layout of bits in a memory word, the layout of memory words in a region, the layout of regions in an address space, or even the layout of address spaces in a multiprocessing environment. We provide a semantics for our formulas and then apply the semantics and logic to the task of developing a type system for Mini-KAM, a simplified version of the abstract machine used in the ML Kit with regions.
This is joint work with Limin Jia and David Walker.