Difference between revisions of "TACL Seminar Spring '03"

From CSWiki
Jump to: navigation, search
m (Spring '03 Schedule)
m (Spring '03 Schedule)
Line 8: Line 8:
 
| Feb 24 || Amal Ahmed || Reasoning about Hierarchical Storage || [[TACL_Seminar_Spring_'03#Amal_Ahmed | Abstract]]
 
| Feb 24 || Amal Ahmed || Reasoning about Hierarchical Storage || [[TACL_Seminar_Spring_'03#Amal_Ahmed | Abstract]]
 
|-
 
|-
| Mar 24 || Koji Hasebe - Keito Univ || A Logical Verification Method for Security Protocols
+
| Mar 24 || Koji Hasebe - Keito Univ || A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic || [[TACL_Seminar_Spring_'03#Koji_Hasebe | Abstract]]
Based on Linear Logic and BAN Logic || [[TACL_Seminar_Spring_'03#Koji_Hasebe | Abstract]]
 
 
|}
 
|}
  

Revision as of 03:37, 27 August 2006

TACL Seminar

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.


TACL Seminar