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.
|
