Chuck Thacker is building a new research computer called the BEE3. There was a time, years ago, when computer architecture was a most exciting area to explore. Talented, young computer scientists labored on the digital frontier to devise the optimal design, structure, and implementation of computer systems. The crux of that work led directly to the PC revolution from which hundreds of millions benefit today. Computer architecture was sexy. These days? Not so much. But Chuck Thacker aims to change that.
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction. Now available: Isabelle2008 Some notable improvements: * HOL: significant speedup of Metis prover; proper support for multithreading. * HOL: new version of primrec command supporting type-inference and local theory targets. * HOL: improved support for termination proofs of recursive function definitions. * New local theory targets for class instantiation and overloading. * Support for named dynamic lists of theorems.
The JWIG project investigates design of high-level languages and program analyses for server-oriented Web application programming. JWIG is a Java-based descendant of <bigwig>, which in turn was inspired by MAWL. The current version of JWIG provides: * a flexible method for dynamically generating XHTML documents using a unique template mechanism based on XACT, * a convenient programming model for working with form input, including declarative form field validation using PowerForms, * an explicit language-based model of sessions, and * program analyses that at compile-time guarantee that all documents being generated dynamically are valid XHTML 1.0 and that form input fields always match the code that receives the input.
[TIMe - eMBEdded - Reactive] Timber is a general programming language specifically aimed at the construction of complex event-driven systems. It allows programs to be conveniently structured in terms of objects and reactions, and the real-time behavior of reactions can furthermore be precisely controlled via platform-independent timing constraints. This property makes Timber particularly suited to both the specification and the implementation of real-time embedded systems. Timber is deeply rooted in the functional programming tradition, although it also draws heavily on object-oriented concepts, and has the notion of concurrent execution built into its core.
My thesis clarified the relationships between existing dialects of ML and studied extending ML with support for recursive modules. Solve a critical problem involving the interaction of recursion and data abstraction known as the double vision problem. In other work with Bob Harper and Manuel Chakravarty, I showed how to extend ML with support for overloading and ad hoc polymorphism through Haskell-style type classes. This work exposes connections between ML modules and Haskell type classes, resulting in a unifying account of the two features Andreas and I have developed a novel module system design that addresses one of the key remaining problems with recursive modules, namely separate compilation. This design seamlessly integrates elements of both traditional ML module systems and Bracha-style mixin modules, resulting in a minimalist account of the ML module system that unifies features. A prototype is available
Daniel Fridlender Mia Indrika March 2001 Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus
ATS is a PL with a highly expressive type system from the framework Applied Type System. Both dependent types and linear types are available in ATS. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ and supports * Functional programming. ATS uses eager call-by-value eval, it also supports lazy call-by-need evaluation. Linear types in ATS can often make FP run with high efficiency * Imperative programming. While features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory mgmt) are allowed in ATS, the type system of ATS is still able to guarantee that no run-time errors can occur * Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads and parallel let * Modular programming. The module system of ATS is largely infuenced by that of Modula-3