ColloquiaTTI-C Talk by Zhong Shao on 2/5/03

[Meridel Trimble]

--------------------------------------------------------------- 
TOYOTA TECHNOLOGICAL INSTITUTE - TALK 
--------------------------------------------------------------- 

Date: Wednesday, February 5th, 2003 

Time: 2:30 p.m. 

Place: Ryerson Hall 251 

Speaker: Zhong Shao, Yale University 

Title: Towards a Principled Multi-Language Infrastructure  

------------------------------------- 
Abstract: 

Component software platforms, such as Microsoft's .NET Common Language 
Runtime (CLR), provide a secure virtual machine in which components 
developed independently can smoothly interoperate.  CLR supports 
flexible interoperation by compiling various source languages into a 
common intermediate language and by using a unified type system. 
However, the type system in CLR (and Java VM) enforces only 
conventional type safety in an object-oriented system.  Therefore, 
higher-level specifications (e.g., resource bounds, generalized access 
control, formal software protocols) cannot be enforced. Because 
conventional type systems are too inflexible for real applications, 
developers often bypass the type system, producing code that steps 
outside the managed part of the VM; such components cannot be verified. 

At Yale we have been developing typed common intermediate languages 
(named FLINT) that can support safely not only the standard 
object-oriented model, but also higher-order generic (polymorphic) 
programming and Java-style reflection (introspection). Unlike CLR, our 
type system is independent of any particular programming model, yet it 
is capable of expressing all valid propositions and proofs in 
higher-order predicate logic (so it can be used to capture and verify 
advanced program properties).  The rich type system of FLINT makes it 
possible to typecheck both compiler intermediate code and low level 
machine code; this allows typechecking to take place at any phase of 
compilation, even after optimizations and register allocation. It also 
leads to a smaller and more extensible VM because low-level native 
routines that would otherwise be in VM can now be verified and moved 
into a certified library.  This talk describes our vision of the FLINT 
system, outline our approach to its design, and survey the technologies 
that can be brought to support its implementation.
-------------------------------------------------- 

*The talk will be followed by refreshments in Ryerson 255* 

If you would like to meet with the speaker, please send e-mail to Meridel 
Trimble: mtrimble at tti-c.org