OOPSLA '04

Program
Technical Program
  Invited Speakers
  Technical Papers
  Onward!
  Panels
  Practitioner Reports
  Tutorials
Workshops
DesignFest
Educators' Symposium
Demonstrations
Posters
Doctoral Symposium
Exhibits
Student Research Comp.
FlashBoF
 
Turing Lecture
 
Social Events
 
Week at a Glance
 
Final Program (1.5M .pdf)

Find in Program
 

Page
Printer-friendly

Basket
view, help

"Languages of the Future"
Object-Oriented Programming, Systems, Languages and Applications
Home    Program    Housing & Transportation    Registration    Submissions    Wiki    Maps
 
  > Technical Program > Onward! > Rethinking Languages

 : Thursday

Languages of the Future

Ballroom C
Thursday, 9:15, 45 minutes
 


 
7·8·9·10·11·12·13·14·15·16·17·18·19·20·21

Tim Sheard, OGI School of Science & Engineering, Oregon Health & Science University

This paper explores a new point in the design space of formal reasoning systems—part programming language, part logical framework. The system is built on a programming language where the user expresses equality constraints between types and the type checker then enforces these constraints. This simple extension to the type system allows the programmer to describe properties of his program in the types of witness objects which can be thought of as concrete evidence that the program has the property desired. These techniques and two other rich typing mechanisms, rank-N polymorphism and extensible kinds, create a powerful new programming idiom for writing programs whose types enforce semantic properties.

A language with these features is both a practical programming language and a logic. This marriage between two previously separate entities increases the probability that users will apply formal methods to their programming designs. This kind of synthesis creates the foundations for the languages of the future.