Welcome to the Tool and Algorithms for Compilers and Languages (TACL) Seminar of the Computer Science department of Princeton University.
- Program optimization
- Program analysis
- Compiler-hardware interfaces
- Run-time systems
- Virtual machines
- Type systems
- Domain-specific programming languages
- Program logics, or logics in general,
- Software engineering and language design,
- Programming language semantics
- Language-based security.
Seminars are also announced on the TACL mailing list. If you are giving a talk, send your abstract to the list a day or so in advance.
Fall '06 Schedule
|Sep 27||Limin Jia||Linear Logic and Imperative Programming||Abstract|
|Oct 13||Northeastern Verification Seminar (X-NEVER)|
|Oct 19||New Jersey Programming Languages and Systems Seminar (NJPLS)|
|Nov 13||Stevens / Columbia / IBM Research - Security and Privacy Day|
Linear Logic and Imperative Programming
A large part of programming language research is to develop new language features and tools that help programmers write more reliable code. One of the most important and enduring problems in programming languages research involves verification of programs that construct, manipulate and dispose of complex heap-allocated data structures. Over the last several years, great progress has been made on this problem by using substructural logics to specify the shape of heap-allocated data structures. These logics can capture aliasing properties in a substantially more concise notation than is possible in conventional logics.
In this dissertation, we present our work on using an extension of Girard's intuitionistic linear logic (a substructural logic) with classical constraints as the base logic to reason about the memory safety and shape invariants of programs that manipulate complex heap-allocated data structures.
The main contribution of this thesis is the idea of incorporating high-level linear logical formulas into imperative languages; either as dynamic contract specifications, which allow clear, compact and semantically well-defined documentation of heap-shape properties; or as language constructs, which drive safe construction and manipulation of sophisticated heap-allocated data structures.