TACL Seminar Fall '04
Fall '04 Schedule
|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|
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.
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.
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.