Contents of this page: Local information | Proposed topics for discussion | Proposed talksMinutes of the meeting are now available (last updated 2nd May 2003).
Robert Dewar has very kindly offered his apartment for the meeting. This is at 73, 5th Avenue, which is between 15th and 16th streets and near Union Square, despite what some mapping software will tell you.
Accommodation is on a do-it-yourself basis. We expect that you will be able to arrange good value flight-plus-hotel deals through a real or virtual travel agent. More detailed travel information is on Annie Liu's local page.
Johan reckons there's a common interest, with his Proxima system, Bernhard Möller's Java Power Presenter, Roland Backhouse's MathSpad, the Cornell Synthesizer Generator, etc.
A long time ago, we created a set of conceptually simple but challenging problems, and for a sequence of meetings a large part was devoted to presenting diverse approaches to these problems, thereby highlighting strengths and weaknesses of various methods and formalisms. I propose to make a new repository of challenge problems that can serve as a source of inspiration for the Group.
No abstract provided.
No abstract provided.
No abstract provided.
The Abstract State Machine Language (AsmL) is a novel, executable modeling language which is fully integrated in the .NET framework and Microsoft development tools. AsmL also supports model-based testing, i.e. where the model is used to derive test cases and a test oracle. This presentation covers the rational of why we build AsmL and we show its use for modeling and testing components and protocols.
NN adds native support for XML and SQL programming to C#. A unified type system bridges the gap between the seemingly different worlds of semi-structured hierarchical data, relational data and object-oriented class hierarchies. XML values can be denoted, passed around, queried or updated, all in a type-safe way. NN also supports SQL queries, irrespective of whether the data is in memory or on the disk. This presentation covers NN's design goals, type system, language features, and extensibility model, and demonstrates some NN samples running in Visual Studio .NET.
Doug Smith and I are working (with others from Kestrel) on the application of Specware concepts to imperative programming. Doug will present a solution to the garbage-collection problem using their especs (which base on Abstract State Machines), while I am basing the solution on monads. It may be interesting to see these two approaches side-by-side.
Roland Backhouse and I have recently had a research proposal accepted for a project called Datatype-Generic Programming, which is to develop a novel mechanism for parametrization based on higher-order (but not quite parametric) polymorphism. The project has yet to start, but I can describe our intentions and expectations.
At Meeting 56, I gave necessary and sufficient conditions for when a partial function can be written as a fold or an unfold. I had only ugly set-theoretic proofs of the results. I now have elegant relational proofs of these and some related results (about injections, the duals of partial functions), which I can report.
There is a well-known "folklore" functional program for the Sieve of Eratosthenes. I present a calculational derivation, based on the universal property of streams.
While there are many special ways to specify analysis of complex data, relational rules simplify and generalize them. Such rules are used explicitly or implicitly in business processes, biological analysis, analysis of computer programs, and many other applications. Programming each kind of analysis by hand is a daunting recurring task, but doing the analysis using a general evaluator program on any particular set of rules incurs a significant overhead and does not provide good performance guarantees. We have developed a method for automatically generating efficient specialized programs for analysis problems specified using Datalog, a general logic database query language based on relational rules. The method provides precise guarantees for both the running time and space consumption for the generated analysis programs.This result is based on a general transformational method that makes computation proceed in an iterative and incremental fashion, analogous to integration by differentiation in calculus. The method also exploits sophisticated structures for storing and accessing complex data. Both time and space complexities of the generated programs are optimal in a precisely defined sense. We apply the method to a number of analysis problems, some with improved time complexities and all with greatly improved algorithm understanding and greatly simplified complexity analysis.
(joint work with Scott Stoller)
No abstract provided.
I will give an overview of program synthesis, and verification and validation work in the Automated Software Engineering group at NASA Ames Research Center. This will include a description of a system for synthesis of Kalman Filter state estimation code, certified synthesis of integrated Kalman Filter code and Stateflow diagrams, work on runtime analysis, and efforts to infuse this technology into NASA missions.