Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program.We describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated as part of the DML project. When used with a simple set of bounds checking qualifiers, Dsolve reduces manual annotation required from 31% of program text to under 1%.
I didn't see anyone post them yet, so here are the slides from Tim Sweeney's POPL talk entitled "The Next Mainstream Programming Languages: A Game Developer's Perspective". I know Tim and I aren't the only game developers who follow LtU, and I figure even non-game developers might find them quite interesting!
concurrent paradigm, namely functional programming extended with threads and ports, which I call multi-agent dataflow programming. * The declarative concurrent subset (no ports) has no race conditions and can be programmed like a functional language. The basic concept is dataflow synchronization of single-assignment variables. A useful data structure is the stream, a list with dataflow tail used as a communication channel. * Nondeterminism can be added exactly where needed and minimally, by using ports - a named stream to which any thread can send. * All functional building blocks are concurrency patterns. Map, fold, filter, etc., are all useful for building concurrent programs. * Concurrent systems can be configured in any order and concurrently with actual use of the system. * Designing concurrent programs is any declarative part of the program can be put in own thread, loosening the coupling between system's parts * The paradigm is easily extended
As part of a larger project, we have built a declarative assembly language. This language enables us to specify multiple code paths to compute particular quantities, giving the instruction scheduler more flexibility in balancing execution resources for superscalar execution. The instruction scheduler is also innovative in that it includes aggressive pipelining, and exhaustive (but lazy) search for optimal instruction schedules. We present some examples where our approach has produced very promising results. I think this paper is a nice followup to the recent discussion of SPE because it goes further than that paper by analyzing what data are necessary to achieve the ultimate goal of optimal or near-optimal instruction scheduling on superscalar architectures. In other words, it strongly suggests that we can do better than simply embedding low-level instructions in a high-level language by instead embedding a graph of desired results (vertices) and instructions for reaching them
Total Functional Programming Here's an interesting paper recently mention in another thread: Total Functional Programming... Abstract: The driving idea of functional programming is to make programming more closely related to mathematics. A program in a functional language such as Haskell or Miranda consists of equations which are both computation rules and a basis for simple algebraic reasoning about the functions and data structures they define. The existing model of functional programming, although elegant and powerful, is compromised to a greater extent than is commonly recognized by the presence of partial functions. We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. Among other things this requires a type distinction between data, which is finite, and codata, which is potentially infinite. I presume that the bogus definiton of "fib" is a subtle reminder of the importance of eliminating bottom.
Does anyone know of work done on co-data-types? There has been a lot of work done on co-data and stream programming, but the assumption is usually of a very simple repetitive data stream. Has anyone done any work on highly structured co-data or co-data-types? A data structure passed into a function represents a limit on all of it's constituent types, that is, the structure must be fully constructed (AND logic) before the function can be called. But a co-data structure (co-type) passed into a function represents a co-limit and only needs to be partially constructed (OR logic), perhaps the function can even return partial (co-data) results based upon the co-data-type it receives. This seems to me a very relevant topic for advancing stream programming and the exploitation of multiple layers of data parallelism.