TACL Seminar Fall '04

From CSWiki
Revision as of 22:55, 24 July 2007 by Gewang (talk | contribs) (reverting from spam attack)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

TACL Seminar

Fall '04 Schedule

Date Speaker Title Links
Aug 12 Xinming Ou Dynamic Typing with Dependent Types Abstract / Paper
Oct 1 New Jersey Programming Languages and Systems Seminar (NJPLS)
Dec 3 New Jersey Programming Languages and Systems Seminar (NJPLS)
Dec 7 Adrian Francalanza (Sussex) On Increasing the Reliability of Distributed Software Abstract
Jan 10 Frances Perry Micro-CLI Abstract

Abstracts

Xinming Ou

Dynamic Typing with Dependent Types

Dependent type systems are promising tools programmers can use to increase the reliability and security of their programs. Unfortunately, dependently-typed programming languages require programmers to annotate their programs with many typing specifications to help guide the type checker. This paper shows how to make the process of programming with dependent types more palatable by defining a language in which programmers have fine-grained control over the trade-off between the number of dependent typing annotations they must place on programs and the degree of compile-time safety. More specifically, certain program fragments are marked "dependent", in which case the programmer annotates them in detail and adependent type checker verifies them at compile time. Other fragments are marked "simple", in which case they may be annotation-free and dependent constraints are verified at run time.

TCS '04 Paper

Adrian Francalanza

On Increasing the Reliability of Distributed Software

Distributed programming is more complex that programming for a standalone machine because of aspects such as asynchronous threads executing at distinct nodes and the occurrence of partial failure for subsets of the nodes. As a result, it is harder to produce dependable distributed software. In this talk, we propose different ways how to increase the dependability of distributed software.

We start by reviewing Milner's \pi-calculus, which elegantly describes the execution of parallel threads that occasionally synchronise between themselves for communication purposes. We then extend this language by distributing threads across named locations that may permanently fail in fail-stop fashion.

We subsequently discuss ways how to increase the dependability of software written in our distributed pi-calculus. These include restricting the visibility and usage of certain resources through types, developing an equational theory for this language and use this theory to define measures of reliability, that guarantees continuous delivery of correct behaviour for our distributed pi-calculus programs in the presence of failure.

Throughout the talk we make extensive use of programming examples to elucidate the concepts presented. No prior knowledge of the \pi-calculus will be assumed.

Frances Perry

Micro-CLI

We describe an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the Common Language Infrastructure. We show how to compile well-typed Micro-CLI into well-typed assembly.



TACL Seminar